--- a/src/Tools/jEdit/etc/options Mon Sep 10 21:15:46 2012 +0200
+++ b/src/Tools/jEdit/etc/options Mon Sep 10 21:17:32 2012 +0200
@@ -13,7 +13,10 @@
-- "tooltip font size (according to HTML)"
option jedit_tooltip_margin : int = 60
- -- "margin for tooltip pretty-printing (in characters)"
+ -- "margin for tooltip pretty-printing"
option jedit_tooltip_dismiss_delay : real = 8.0
- -- "global delay for Swing tooltips (in seconds)"
+ -- "global delay for Swing tooltips"
+
+option jedit_load_delay : real = 0.5
+ -- "delay for file load operations (new buffers etc.)"