src/Tools/jEdit/etc/options

--- a/src/Tools/jEdit/etc/options	Fri Oct 05 14:51:33 2012 +0200
+++ b/src/Tools/jEdit/etc/options	Fri Oct 05 18:01:48 2012 +0200
@@ -15,9 +15,6 @@
 option jedit_tooltip_margin : int = 60
   -- "margin for tooltip pretty-printing"
 
-option jedit_tooltip_dismiss_delay : real = 8.0
-  -- "global delay for Swing tooltips"
-
 option jedit_text_overview : bool = true
   -- "paint text overview column (potentially slow for large files)"