src/Tools/jEdit/etc/options

--- a/src/Tools/jEdit/etc/options	Tue Sep 11 11:53:34 2012 +0200
+++ b/src/Tools/jEdit/etc/options	Tue Sep 11 15:47:42 2012 +0200
@@ -18,5 +18,8 @@
 option jedit_tooltip_dismiss_delay : real = 8.0
   -- "global delay for Swing tooltips"
 
+
+section {* Reactivity *}
+
 option jedit_load_delay : real = 0.5
   -- "delay for file load operations (new buffers etc.)"