more generous margin;
authorwenzelm
Thu, 10 Nov 2011 22:39:32 +0100
changeset 45446 d29d73117b73
parent 45445 41e641a870de
child 45447 a97251eea458
more generous margin;
src/Tools/jEdit/src/Isabelle.props
--- a/src/Tools/jEdit/src/Isabelle.props	Thu Nov 10 22:32:10 2011 +0100
+++ b/src/Tools/jEdit/src/Isabelle.props	Thu Nov 10 22:39:32 2011 +0100
@@ -30,7 +30,7 @@
 options.isabelle.tooltip-font-size.title=Tooltip Font Size
 options.isabelle.tooltip-font-size=10
 options.isabelle.tooltip-margin.title=Tooltip Margin
-options.isabelle.tooltip-margin=40
+options.isabelle.tooltip-margin=60
 options.isabelle.tooltip-dismiss-delay.title=Tooltip Dismiss Delay (global)
 options.isabelle.tooltip-dismiss-delay=8.0
 options.isabelle.startup-timeout=25.0