changeset 56876 | f12f7c6dd83d |
parent 56843 | b2bfcd8cda80 |
child 56883 | 38c6b70e5e53 |
--- a/src/Tools/jEdit/etc/options Tue May 06 16:05:14 2014 +0200 +++ b/src/Tools/jEdit/etc/options Tue May 06 16:08:07 2014 +0200 @@ -52,7 +52,7 @@ -- "insert uniquely completed abbreviation immediately into buffer" public option jedit_completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store" - -- "glob patterns to ignore in path completion (separated by colons)" + -- "glob patterns to ignore in file-system path completion (separated by colons)" section "Spell Checker"