.hgignore
author wenzelm
Mon, 28 Jan 2013 15:45:54 +0100
changeset 52035 8c534a166f2d
parent 49988 fcd21f714996
child 52054 8c7f0f37a3ab
child 55270 a556fcaf2ae3
child 55317 4300525448d7
child 55933 7f36da77130d
permissions -rw-r--r--
Added tag Isabelle2013-RC2 for changeset 7fc61bfb1c2d
wenzelm@28909
     1
syntax: glob
wenzelm@28909
     2
wenzelm@28909
     3
*~
wenzelm@28911
     4
*.class
wenzelm@28911
     5
*.jar
wenzelm@49823
     6
*.orig
wenzelm@49823
     7
*.rej
wenzelm@28909
     8
.DS_Store
wenzelm@28909
     9
wenzelm@28909
    10
wenzelm@28909
    11
syntax: regexp
wenzelm@28909
    12
haftmann@31669
    13
^contrib
wenzelm@28909
    14
^heaps/
wenzelm@28909
    15
^browser_info/
wenzelm@49988
    16
^doc/.*\.dvi
wenzelm@49988
    17
^doc/.*\.eps
wenzelm@49988
    18
^doc/.*\.pdf
wenzelm@49988
    19
^doc/.*\.ps
wenzelm@44167
    20
^src/Tools/jEdit/dist/