src/Tools/jEdit/etc/options

--- a/src/Tools/jEdit/etc/options	Sat Nov 24 17:05:10 2012 +0100
+++ b/src/Tools/jEdit/etc/options	Sat Nov 24 17:12:06 2012 +0100
@@ -18,6 +18,9 @@
 option jedit_text_overview_limit : int = 100000
   -- "maximum amount of text to visualize in overview column"
 
+option jedit_symbols_search_limit : int = 50
+  -- "maximum number of symbols in search result"
+
 
 section "Rendering of Document Content"