| changeset 56326 | c3d7b3bb2708 |
| parent 56202 | 0a11d17eeeff |
| child 56550 | b26bdc1f96e5 |
--- a/src/Tools/jEdit/etc/options Sun Mar 30 20:23:26 2014 +0200 +++ b/src/Tools/jEdit/etc/options Sun Mar 30 21:03:40 2014 +0200 @@ -46,7 +46,7 @@ -- "delay for completion popup (seconds)" public option jedit_completion_immediate : bool = false - -- "insert unique completion immediately into buffer (if delay = 0)" + -- "insert uniquely completed abbreviation immediately into buffer" section "Rendering of Document Content"