diff -r 70b7e91fa1f9 -r 39708e59f4b0 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Sun Feb 16 21:33:28 2014 +0100
+++ b/src/Tools/jEdit/etc/options	Mon Feb 17 11:14:26 2014 +0100
@@ -76,6 +76,7 @@
 option intensify_color : string = "FFCC6664"
 option quoted_color : string = "8B8B8B19"
 option antiquoted_color : string = "FFC83219"
+option antiquote_color : string = "6600CCFF"
 option highlight_color : string = "50505032"
 option hyperlink_color : string = "000000FF"
 option active_color : string = "DCDCDCFF"