From 8c0bc2f5e51b6037868a4dcab612390e67136be0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 17 Feb 2015 16:03:40 +0100
Subject: Fixing bug #4023 again.

---
 ide/coqide.ml | 1 +
 1 file changed, 1 insertion(+)

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];
-- 
cgit v1.2.3