--- a/src/Tools/jEdit/etc/options Tue Aug 27 14:56:11 2013 +0200
+++ b/src/Tools/jEdit/etc/options Tue Aug 27 15:35:51 2013 +0200
@@ -9,12 +9,12 @@
public option jedit_font_scale : real = 1.0
-- "scale factor of add-on panels wrt. main text area"
+public option jedit_popup_font_scale : real = 0.85
+ -- "scale factor of popups wrt. main text area"
+
public option jedit_tooltip_delay : real = 0.75
-- "open/close delay for document tooltips"
-public option jedit_tooltip_font_scale : real = 0.85
- -- "scale factor of tooltips wrt. main text area"
-
public option jedit_tooltip_margin : int = 60
-- "margin for tooltip pretty-printing"