diff options
| author | Pierre-Marie Pédrot | 2015-02-17 16:03:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-17 16:03:40 +0100 |
| commit | 8c0bc2f5e51b6037868a4dcab612390e67136be0 (patch) | |
| tree | 36ffc421faedb6445ebdbb54c0b89843c481851d | |
| parent | 52464172064fa66b1bb85d34e0062be04b2ecf97 (diff) | |
Fixing bug #4023 again.
| -rw-r--r-- | ide/coqide.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 4ca99256a1..cb05363ddc 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -852,6 +852,7 @@ let refresh_editor_prefs () = Tags.set_processing_color (Tags.color_of_string current.processing_color); Tags.set_processed_color (Tags.color_of_string current.processed_color); Tags.set_error_color (Tags.color_of_string current.error_color); + Tags.set_error_fg_color (Tags.color_of_string current.error_fg_color); sn.script#misc#modify_base [`NORMAL, `COLOR clr]; sn.proof#misc#modify_base [`NORMAL, `COLOR clr]; sn.messages#misc#modify_base [`NORMAL, `COLOR clr]; |