| changeset 51452 | 14e6d761ba1c |
| parent 51441 | 37f699750430 |
| child 51533 | 3f6280aedbcc |
--- a/src/Tools/jEdit/etc/options Mon Mar 18 11:04:59 2013 +0100 +++ b/src/Tools/jEdit/etc/options Mon Mar 18 11:29:50 2013 +0100 @@ -7,7 +7,7 @@ -- "scale factor of add-on panels wrt. main text area" option jedit_tooltip_delay : real = 0.75 - -- "delay for semantic tooltip popup" + -- "open/close delay for document tooltips" option jedit_tooltip_font_scale : real = 0.85 -- "scale factor of tooltips wrt. main text area"