# HG changeset patch
# User wenzelm
# Date 1377806009 -7200
# Node ID 814eee60e1b15d9bf859535e0120c8980f229885
# Parent  fd27b8f5a479d41d8cbb2203261adc9931fd5d24
tuned;

diff -r fd27b8f5a479 -r 814eee60e1b1 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"