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"