src/Tools/jEdit/etc/options

--- a/src/Tools/jEdit/etc/options	Thu Aug 29 20:46:55 2013 +0200
+++ b/src/Tools/jEdit/etc/options	Thu Aug 29 21:17:46 2013 +0200
@@ -39,6 +39,9 @@
 public option jedit_completion_delay : real = 0.0
   -- "delay for completion popup (seconds)"
 
+public option jedit_completion_immediate : bool = false
+  -- "insert unique completion immediately into buffer (if delay = 0)"
+
 
 section "Rendering of Document Content"