| changeset 50498 | 6647ba2775c1 |
| parent 50450 | 358b6020f8b6 |
| child 50499 | f496b2b7bafb |
--- a/src/Tools/jEdit/etc/options Wed Dec 12 19:03:49 2012 +0100 +++ b/src/Tools/jEdit/etc/options Wed Dec 12 21:50:42 2012 +0100 @@ -43,6 +43,7 @@ option hyperlink_color : string = "000000FF" option active_color : string = "DCDCDCFF" option active_hover_color : string = "9DC75DFF" +option active_result_color : string = "666633FF" option keyword1_color : string = "006699FF" option keyword2_color : string = "009966FF"