changeset 49296 | 313369027391 |
parent 49295 | 2750756db9c5 |
child 49355 | 7d1af0a6e797 |
--- a/src/Tools/jEdit/etc/options Tue Sep 11 22:59:25 2012 +0200 +++ b/src/Tools/jEdit/etc/options Tue Sep 11 23:26:03 2012 +0200 @@ -19,7 +19,7 @@ -- "global delay for Swing tooltips" -section "Editor Document View" +section "Rendering of Document Content" option color_outdated : string = "EEE3E3FF" option color_unprocessed : string = "FFA0A0FF"