| changeset 54377 | 750561986828 |
| parent 53914 | 48072f049838 |
| child 54881 | dff57132cf18 |
--- a/src/Tools/jEdit/etc/options Fri Nov 08 15:10:16 2013 +0100 +++ b/src/Tools/jEdit/etc/options Fri Nov 08 17:34:37 2013 +0100 @@ -42,6 +42,9 @@ public option jedit_completion_delay : real = 0.0 -- "delay for completion popup (seconds)" +public option jedit_completion_dismiss_delay : real = 0.0 + -- "delay for dismissing obsolete completion popup (seconds)" + public option jedit_completion_immediate : bool = false -- "insert unique completion immediately into buffer (if delay = 0)"