src/Tools/jEdit/etc/options

--- a/src/Tools/jEdit/etc/options	Sat Sep 19 20:38:28 2015 +0200
+++ b/src/Tools/jEdit/etc/options	Sat Sep 19 20:47:11 2015 +0200
@@ -30,9 +30,6 @@
 public option jedit_tooltip_margin : int = 60
   -- "margin for tooltip pretty-printing"
 
-public option jedit_text_overview_limit : int = 65536
-  -- "maximum amount of text to visualize in overview column"
-
 public option jedit_structure_limit : int = 1000
   -- "maximum number of lines to scan for language structure"