tuned magic number, for improved reactivity on old 2-core machine;
authorwenzelm
Sat, 14 Sep 2013 22:50:15 +0200
changeset 53639 09a4954e7c07
parent 53638 203794e8977d
child 53640 3170b5eb9f5a
tuned magic number, for improved reactivity on old 2-core machine;
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