diff -r 2750756db9c5 -r 313369027391 src/Tools/jEdit/etc/options
--- 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"