| changeset 56170 | 638b29331549 |
| parent 56064 | 7658489047e3 |
| child 56197 | 416f7a00e4cb |
--- a/src/Tools/jEdit/etc/options Mon Mar 17 10:11:23 2014 +0100 +++ b/src/Tools/jEdit/etc/options Mon Mar 17 10:45:29 2014 +0100 @@ -42,7 +42,7 @@ public option jedit_completion : bool = true -- "enable completion popup" -public option jedit_completion_delay : real = 0.0 +public option jedit_completion_delay : real = 0.5 -- "delay for completion popup (seconds)" public option jedit_completion_dismiss_delay : real = 0.0