aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-02-14 19:00:38 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-02-14 19:00:38 +0100
commit2bea61e8e1ec02906bf63db4142cb26528bb4d76 (patch)
tree629ab9f113a3222b22f8e024e104e0ba18c452f8 /ide
parent12a5ccdf1cb69c745aa72dad923349d411682f8d (diff)
CoqIDE: restore old default colors
Diffstat (limited to 'ide')
-rw-r--r--ide/tags.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/tags.ml b/ide/tags.ml
index 40d5b4ded..079cf9485 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -16,8 +16,8 @@ let make_tag (tt:GText.tag_table) ~name prop =
(* These work fine for colorblind people too *)
let default_processed_color = "light green"
let default_processing_color = "light blue"
-let default_error_color = "#FF3333"
-let default_error_fg_color = "#FF5555"
+let default_error_color = "#FFCCCC"
+let default_error_fg_color = "red"
let default_color = "cornsilk"
let processed_color = ref default_processed_color