.hgignore
author wenzelm
Sat, 05 Jul 2014 16:29:19 +0200
changeset 58865 1767b0f3b29b
parent 57761 f47de9e82b0f
child 59104 09a9b04605e5
permissions -rw-r--r--
Added tag Isabelle2014-RC0 for changeset 251ef0202e71
     1 syntax: glob
     2 
     3 *~
     4 *.class
     5 *.jar
     6 *.marks
     7 *.orig
     8 *.rej
     9 .DS_Store
    10 .swp
    11 
    12 
    13 syntax: regexp
    14 
    15 ^contrib
    16 ^heaps/
    17 ^browser_info/
    18 ^doc/.*\.dvi
    19 ^doc/.*\.eps
    20 ^doc/.*\.pdf
    21 ^doc/.*\.ps
    22 ^src/Tools/jEdit/dist/