# HG changeset patch
# User wenzelm
# Date 1379191815 -7200
# Node ID 09a4954e7c07ee31801bd0bcec0b1616df9f3807
# Parent  203794e8977d2699977ba1f8c8643f3e16cdf499
tuned magic number, for improved reactivity on old 2-core machine;

diff -r 203794e8977d -r 09a4954e7c07 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Sat Sep 14 22:30:10 2013 +0200
+++ b/src/Tools/jEdit/etc/options	Sat Sep 14 22:50:15 2013 +0200
@@ -21,7 +21,7 @@
 public option jedit_tooltip_margin : int = 60
   -- "margin for tooltip pretty-printing"
 
-public option jedit_text_overview_limit : int = 100000
+public option jedit_text_overview_limit : int = 65536
   -- "maximum amount of text to visualize in overview column"
 
 public option jedit_symbols_search_limit : int = 50