src/Tools/jEdit/etc/options

--- a/src/Tools/jEdit/etc/options	Sat May 03 20:31:29 2014 +0200
+++ b/src/Tools/jEdit/etc/options	Sat May 03 22:47:43 2014 +0200
@@ -51,6 +51,9 @@
 public option jedit_completion_immediate : bool = false
   -- "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)"
+
 
 section "Spell Checker"