# HG changeset patch
# User wenzelm
# Date 1394045861 -3600
# Node ID fd5e3f93bae45167464c84c713ac7d7c34e5214f
# Parent  4bdae9403baff1206552410efdd9fea6a3901516
tuned color (cf. jEdit FUNCTION);

diff -r 4bdae9403baf -r fd5e3f93bae4 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Wed Mar 05 19:52:28 2014 +0100
+++ b/src/Tools/jEdit/etc/options	Wed Mar 05 19:57:41 2014 +0100
@@ -84,7 +84,7 @@
 option keyword1_color : string = "006699FF"
 option keyword2_color : string = "009966FF"
 option keyword3_color : string = "0099FFFF"
-option quasi_keyword_color : string = "66CCFFFF"
+option quasi_keyword_color : string = "9966FFFF"
 option caret_invisible_color : string = "50000080"
 option completion_color : string = "0000FFFF"