changeset 53294 | 814eee60e1b1 |
parent 53292 | f567c1c7b180 |
child 53487 | fc87164e3577 |
--- 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"