src/Tools/jEdit/etc/options

--- a/src/Tools/jEdit/etc/options	Mon Oct 22 14:52:38 2012 +0200
+++ b/src/Tools/jEdit/etc/options	Mon Oct 22 16:27:55 2012 +0200
@@ -15,8 +15,8 @@
 option jedit_tooltip_margin : int = 60
   -- "margin for tooltip pretty-printing"
 
-option jedit_text_overview : bool = true
-  -- "paint text overview column (potentially slow for large files)"
+option jedit_text_overview_limit : int = 100000
+  -- "maximum amount of text to visualize in overview column"
 
 
 section "Rendering of Document Content"