| changeset 55924 | fd5e3f93bae4 |
| parent 55919 | 2eb8c13339a5 |
| child 56064 | 7658489047e3 |
--- a/src/Tools/jEdit/etc/options Wed Mar 05 19:52:28 2014 +0100 +++ b/src/Tools/jEdit/etc/options Wed Mar 05 19:57:41 2014 +0100 @@ -84,7 +84,7 @@ option keyword1_color : string = "006699FF" option keyword2_color : string = "009966FF" option keyword3_color : string = "0099FFFF" -option quasi_keyword_color : string = "66CCFFFF" +option quasi_keyword_color : string = "9966FFFF" option caret_invisible_color : string = "50000080" option completion_color : string = "0000FFFF"