--- a/src/Tools/jEdit/etc/options Tue Dec 30 14:11:06 2014 +0100
+++ b/src/Tools/jEdit/etc/options Tue Dec 30 23:45:03 2014 +0100
@@ -88,12 +88,14 @@
option writeln_color : string = "C0C0C0FF"
option information_color : string = "C1DFEEFF"
option warning_color : string = "FF8C00FF"
+option legacy_color : string = "FF8C00FF"
option error_color : string = "B22222FF"
option writeln_message_color : string = "F0F0F0FF"
option state_message_color : string = "F0E4E4FF"
option information_message_color : string = "DCEAF3FF"
option tracing_message_color : string = "F0F8FFFF"
option warning_message_color : string = "EEE8AAFF"
+option legacy_message_color : string = "EEE8AAFF"
option error_message_color : string = "FFC1C1FF"
option spell_checker_color : string = "0000FFFF"
option bad_color : string = "FF6A6A64"