src/Tools/jEdit/etc/options
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"