From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Jul 2015 10:36:12 +0200 Subject: Imported Upstream version 8.5~beta2+dfsg --- ide/preferences.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'ide/preferences.mli') 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; -- cgit v1.2.3