src/Tools/jEdit/etc/options
changeset 62986 9d2fae6b31cc
parent 62792 340428bebdb8
child 62988 224e8d8a4fb8
     1.1 --- a/src/Tools/jEdit/etc/options	Thu Apr 14 20:47:44 2016 +0200
     1.2 +++ b/src/Tools/jEdit/etc/options	Thu Apr 14 22:55:53 2016 +0200
     1.3 @@ -99,6 +99,8 @@
     1.4  option spell_checker_color : string = "0000FFFF"
     1.5  option bad_color : string = "FF6A6A64"
     1.6  option intensify_color : string = "FFCC6664"
     1.7 +option entity_def_color : string = "CCD9FFA0"
     1.8 +option entity_ref_color : string = "E6FFCCA0"
     1.9  option breakpoint_disabled_color : string = "CCCC0080"
    1.10  option breakpoint_enabled_color : string = "FF9966FF"
    1.11  option quoted_color : string = "8B8B8B19"