# HG changeset patch
# User wenzelm
# Date 1439340039 -7200
# Node ID f39d004f2ff407c7f40a6c652f599de8c8679cfd
# Parent  7432d6bb4195bfefb9fc9cd8010c5d8a4c524234
tuned colors;

diff -r 7432d6bb4195 -r f39d004f2ff4 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Wed Aug 12 02:21:00 2015 +0200
+++ b/src/Tools/jEdit/etc/options	Wed Aug 12 02:40:39 2015 +0200
@@ -100,8 +100,8 @@
 option spell_checker_color : string = "0000FFFF"
 option bad_color : string = "FF6A6A64"
 option intensify_color : string = "FFCC6664"
-option breakpoint_disabled_color : string = "00CC66FF"
-option breakpoint_enabled_color : string = "CC6600FF"
+option breakpoint_disabled_color : string = "CCCC0080"
+option breakpoint_enabled_color : string = "FF9966FF"
 option quoted_color : string = "8B8B8B19"
 option antiquoted_color : string = "FFC83219"
 option antiquote_color : string = "6600CCFF"