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