--- a/src/Tools/jEdit/etc/options Tue Aug 27 15:35:51 2013 +0200
+++ b/src/Tools/jEdit/etc/options Tue Aug 27 16:09:28 2013 +0200
@@ -12,15 +12,15 @@
public option jedit_popup_font_scale : real = 0.85
-- "scale factor of popups wrt. main text area"
+public option jedit_popup_bounds : real = 0.5
+ -- "relative bounds of popup window wrt. logical screen size"
+
public option jedit_tooltip_delay : real = 0.75
-- "open/close delay for document tooltips"
public option jedit_tooltip_margin : int = 60
-- "margin for tooltip pretty-printing"
-public option jedit_tooltip_bounds : real = 0.5
- -- "relative bounds of tooltip window wrt. logical screen size"
-
public option jedit_text_overview_limit : int = 100000
-- "maximum amount of text to visualize in overview column"