| changeset 56064 | 7658489047e3 |
| parent 55924 | fd5e3f93bae4 |
| child 56170 | 638b29331549 |
--- a/src/Tools/jEdit/etc/options Wed Mar 12 16:11:47 2014 +0100 +++ b/src/Tools/jEdit/etc/options Wed Mar 12 16:43:17 2014 +0100 @@ -85,6 +85,7 @@ option keyword2_color : string = "009966FF" option keyword3_color : string = "0099FFFF" option quasi_keyword_color : string = "9966FFFF" +option operator_color : string = "323232FF" option caret_invisible_color : string = "50000080" option completion_color : string = "0000FFFF"