1 files changed, 2 insertions, 0 deletions
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 1b52d20a..1e4f152c 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -32,6 +32,7 @@ type pref =
 
       mutable read_project : project_behavior;
       mutable project_file_name : string;
+      mutable project_path : string option;
 
       mutable encoding : inputenc;
 
@@ -71,6 +72,7 @@ type pref =
       mutable processing_color : string;
       mutable processed_color : string;
       mutable error_color : string;
+      mutable error_fg_color : string;
 
       mutable dynamic_word_wrap : bool;
       mutable show_line_number : bool;