| changeset 55505 | 2a1ca7f6607b |
| parent 55033 | 8e8243975860 |
| child 55526 | 39708e59f4b0 |
--- a/src/Tools/jEdit/etc/options Sat Feb 15 17:10:57 2014 +0100 +++ b/src/Tools/jEdit/etc/options Sat Feb 15 18:28:18 2014 +0100 @@ -83,6 +83,7 @@ option active_result_color : string = "999966FF" option keyword1_color : string = "006699FF" option keyword2_color : string = "009966FF" +option keyword3_color : string = "0099FFFF" option tfree_color : string = "A020F0FF" option tvar_color : string = "A020F0FF"