.hgignore
author wenzelm
Fri, 04 Sep 2015 21:40:59 +0200
changeset 61116 6189d179c2b5
parent 56419 f47de9e82b0f
child 63191 c3896c385c3e
permissions -rw-r--r--
close derivation *before* splitting conjuncts, like Goal.prove_common (see also 757cad5a3fe9) -- potential improvement of performance;

syntax: glob

*~
*.class
*.jar
*.marks
*.orig
*.rej
.DS_Store
.swp


syntax: regexp

^contrib
^heaps/
^browser_info/
^doc/.*\.dvi
^doc/.*\.eps
^doc/.*\.pdf
^doc/.*\.ps
^src/Tools/jEdit/dist/