# HG changeset patch
# User wenzelm
# Date 1399385287 -7200
# Node ID f12f7c6dd83db8ad7ff9c96d8d49865ec99ba3f5
# Parent  f6259d6fb5657ae186c395f68e6c014ae01af97e
tuned;

diff -r f6259d6fb565 -r f12f7c6dd83d src/Tools/jEdit/etc/options
--- 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"