--- a/src/Tools/jEdit/etc/options Tue May 21 13:22:47 2013 +0200
+++ b/src/Tools/jEdit/etc/options Tue May 21 16:47:18 2013 +0200
@@ -52,6 +52,7 @@
option bad_color : string = "FF6A6A64"
option intensify_color : string = "FFCC6664"
option quoted_color : string = "8B8B8B19"
+option antiquoted_color : string = "FFC83219"
option highlight_color : string = "50505032"
option hyperlink_color : string = "000000FF"
option active_color : string = "DCDCDCFF"
@@ -69,6 +70,5 @@
option inner_numeral_color : string = "FF0000FF"
option inner_quoted_color : string = "D2691EFF"
option inner_comment_color : string = "8B0000FF"
-option antiquotation_color : string = "0000FFFF"
option dynamic_color : string = "7BA428FF"