src/Tools/jEdit/etc/options
changeset 60876 52edced9cce5
parent 59753 d743e0e53f41
child 60878 1f0d2bbcf38b
     1.1 --- a/src/Tools/jEdit/etc/options	Mon Aug 10 14:14:49 2015 +0200
     1.2 +++ b/src/Tools/jEdit/etc/options	Mon Aug 10 16:05:41 2015 +0200
     1.3 @@ -100,6 +100,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 breakpoint_color : string = "00CC0032"
     1.8 +option breakpoint_active_color : string = "00CC0064"
     1.9  option quoted_color : string = "8B8B8B19"
    1.10  option antiquoted_color : string = "FFC83219"
    1.11  option antiquote_color : string = "6600CCFF"