--- a/src/Tools/jEdit/etc/options Sat Jul 13 17:05:22 2013 +0200
+++ b/src/Tools/jEdit/etc/options Sat Jul 13 18:13:09 2013 +0200
@@ -42,16 +42,17 @@
option bullet_color : string = "000000FF"
option tooltip_color : string = "FFFFE9FF"
option writeln_color : string = "C0C0C0FF"
+option information_color : string = "C1DFEEFF"
option warning_color : string = "FF8C00FF"
option error_color : string = "B22222FF"
option error1_color : string = "B2222232"
option writeln_message_color : string = "F0F0F0FF"
+option information_message_color : string = "C1DFEE32"
option tracing_message_color : string = "F0F8FFFF"
option warning_message_color : string = "EEE8AAFF"
option error_message_color : string = "FFC1C1FF"
option bad_color : string = "FF6A6A64"
option intensify_color : string = "FFCC6664"
-option information_color : string = "FFCC6632"
option quoted_color : string = "8B8B8B19"
option antiquoted_color : string = "FFC83219"
option highlight_color : string = "50505032"