author | wenzelm |
Sat, 14 Sep 2013 22:50:15 +0200 | |
changeset 53639 | 09a4954e7c07 |
parent 53638 | 203794e8977d |
child 53640 | 3170b5eb9f5a |
--- 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