src/Tools/jEdit/etc/options
changeset 52643 34c29356930e
parent 52576 7f5be9be51a7
child 52644 cea207576f81
--- a/src/Tools/jEdit/etc/options	Sat Jul 13 12:39:45 2013 +0200
+++ b/src/Tools/jEdit/etc/options	Sat Jul 13 13:25:42 2013 +0200
@@ -51,6 +51,7 @@
 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"