src/Tools/jEdit/etc/options

--- a/src/Tools/jEdit/etc/options	Thu Aug 29 21:49:46 2013 +0200
+++ b/src/Tools/jEdit/etc/options	Thu Aug 29 21:53:29 2013 +0200
@@ -33,6 +33,9 @@
 public option jedit_timing_threshold : real = 0.1
   -- "default threshold for timing display"
 
+
+section "Completion"
+
 public option jedit_completion : bool = true
   -- "enable completion popup"