diff options
Diffstat (limited to 'ide/coqide.ml')
| -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 4ca99256a..cb05363dd 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]; |