| changeset 49295 | 2750756db9c5 |
| parent 49294 | a600c017f814 |
| child 49296 | 313369027391 |
--- a/src/Tools/jEdit/etc/options Tue Sep 11 22:54:12 2012 +0200 +++ b/src/Tools/jEdit/etc/options Tue Sep 11 22:59:25 2012 +0200 @@ -19,7 +19,7 @@ -- "global delay for Swing tooltips" -section {* Editor document view *} +section "Editor Document View" option color_outdated : string = "EEE3E3FF" option color_unprocessed : string = "FFA0A0FF"