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"