From 42a71ccbbd2937d270e46c1688b9411a7f82f13d Mon Sep 17 00:00:00 2001 From: Uwe Date: Fri, 4 Mar 2022 04:43:34 +0100 Subject: [PATCH] [Gui] DocumentObserver: re-add a header --- src/Gui/DocumentObserver.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Gui/DocumentObserver.h b/src/Gui/DocumentObserver.h index ed2471b77b..4c550ac620 100644 --- a/src/Gui/DocumentObserver.h +++ b/src/Gui/DocumentObserver.h @@ -23,6 +23,7 @@ #ifndef GUI_DOCUMENTOBSERVER_H #define GUI_DOCUMENTOBSERVER_H +#include #include