src/Tools/jEdit/etc/options
changeset 55033 8e8243975860
parent 54881 dff57132cf18
child 55505 2a1ca7f6607b
--- a/src/Tools/jEdit/etc/options	Fri Jan 17 20:51:36 2014 +0100
+++ b/src/Tools/jEdit/etc/options	Sat Jan 18 19:15:12 2014 +0100
@@ -92,6 +92,7 @@
 option var_color : string = "00009BFF"
 option inner_numeral_color : string = "FF0000FF"
 option inner_quoted_color : string = "D2691EFF"
+option inner_cartouche_color : string = "CC6600FF"
 option inner_comment_color : string = "8B0000FF"
 option dynamic_color : string = "7BA428FF"