src/Tools/jEdit/etc/options
changeset 57833 2c2bae3da1c2
parent 57425 625a369b4f32
child 58750 1b4b005d73c1
--- a/src/Tools/jEdit/etc/options	Thu Jul 31 20:59:10 2014 +0200
+++ b/src/Tools/jEdit/etc/options	Thu Jul 31 21:29:31 2014 +0200
@@ -42,6 +42,12 @@
 public option jedit_completion : bool = true
   -- "enable completion popup"
 
+public option jedit_completion_select_enter : bool = false
+  -- "select completion item via ENTER"
+
+public option jedit_completion_select_tab : bool = true
+  -- "select completion item via TAB"
+
 public option jedit_completion_context : bool = true
   -- "use semantic language context for completion"