src/Tools/jEdit/etc/options

--- a/src/Tools/jEdit/etc/options	Sat Dec 15 20:05:53 2012 +0100
+++ b/src/Tools/jEdit/etc/options	Sat Dec 15 21:07:52 2012 +0100
@@ -12,6 +12,9 @@
 option jedit_tooltip_margin : int = 60
   -- "margin for tooltip pretty-printing"
 
+option jedit_tooltip_bounds : real = 0.5
+  -- "relative bounds of tooltip window wrt. logical screen size"
+
 option jedit_text_overview_limit : int = 100000
   -- "maximum amount of text to visualize in overview column"