src/Tools/jEdit/etc/options

--- a/src/Tools/jEdit/etc/options	Thu Oct 04 11:07:36 2012 +0200
+++ b/src/Tools/jEdit/etc/options	Thu Oct 04 11:39:24 2012 +0200
@@ -18,6 +18,9 @@
 option jedit_tooltip_dismiss_delay : real = 8.0
   -- "global delay for Swing tooltips"
 
+option jedit_text_overview : bool = true
+  -- "paint text overview column (potentially slow for large files)"
+
 
 section "Rendering of Document Content"