src/Tools/jEdit/etc/options

 option jedit_logic : string = ""
   -- "default logic session"
 
 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"
 
 option jedit_tooltip_margin : int = 60