changeset 68871 | f5c76072db55 |
parent 67322 | 734a4e44b159 |
child 69320 | fc221fa79741 |
--- a/src/Tools/jEdit/etc/options Sat Sep 01 18:39:36 2018 +0200 +++ b/src/Tools/jEdit/etc/options Sat Sep 01 20:20:50 2018 +0200 @@ -95,6 +95,7 @@ option error_message_color : string = "FFC1C1FF" option spell_checker_color : string = "0000FFFF" option bad_color : string = "FF6A6A64" +option canceled_color : string = "FF6A6A64" option intensify_color : string = "FFCC6664" option entity_color : string = "CCD9FF80" option entity_ref_color : string = "800080FF"