etc/options
changeset 66158 ad83d4971dfe
parent 65782 4935bac8a850
child 66160 33f759742887
     1.1 --- a/etc/options	Wed Jun 21 21:10:51 2017 +0200
     1.2 +++ b/etc/options	Wed Jun 21 21:55:07 2017 +0200
     1.3 @@ -200,6 +200,9 @@
     1.4  public option completion_limit : int = 40
     1.5    -- "limit for completion within the formal context"
     1.6  
     1.7 +public option completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store"
     1.8 +  -- "glob patterns to ignore in file-system path completion (separated by colons)"
     1.9 +
    1.10  
    1.11  section "Spell Checker"
    1.12