diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-02-14 19:00:38 +0100 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-02-14 19:00:38 +0100 |
commit | 2bea61e8e1ec02906bf63db4142cb26528bb4d76 (patch) | |
tree | 629ab9f113a3222b22f8e024e104e0ba18c452f8 | |
parent | 12a5ccdf1cb69c745aa72dad923349d411682f8d (diff) |
CoqIDE: restore old default colors
-rw-r--r-- | ide/tags.ml | 4 |
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 |