.hgignore
author wenzelm
Sun, 27 Jul 2014 15:40:19 +0200
changeset 59037 f11f3d7589b1
parent 57761 f47de9e82b0f
child 59104 09a9b04605e5
permissions -rw-r--r--
Added tag Isabelle2014-RC1 for changeset c0fd03d13d28
     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/