| changeset 51441 | 37f699750430 |
| parent 51071 | b7e7557e80b5 |
| child 51452 | 14e6d761ba1c |
--- a/src/Tools/jEdit/etc/options Sat Mar 16 17:16:39 2013 +0100 +++ b/src/Tools/jEdit/etc/options Sat Mar 16 21:26:44 2013 +0100 @@ -6,6 +6,9 @@ option jedit_font_scale : real = 1.0 -- "scale factor of add-on panels wrt. main text area" +option jedit_tooltip_delay : real = 0.75 + -- "delay for semantic tooltip popup" + option jedit_tooltip_font_scale : real = 0.85 -- "scale factor of tooltips wrt. main text area"