| changeset 56202 | 0a11d17eeeff |
| parent 56197 | 416f7a00e4cb |
| child 56326 | c3d7b3bb2708 |
--- a/src/Tools/jEdit/etc/options Tue Mar 18 11:27:09 2014 +0100 +++ b/src/Tools/jEdit/etc/options Tue Mar 18 12:25:17 2014 +0100 @@ -82,6 +82,7 @@ option keyword2_color : string = "009966FF" option keyword3_color : string = "0099FFFF" option quasi_keyword_color : string = "9966FFFF" +option improper_color : string = "FF5050FF" option operator_color : string = "323232FF" option caret_invisible_color : string = "50000080" option completion_color : string = "0000FFFF"