.hgignore
author bulwahn
Fri, 11 Mar 2011 10:37:41 +0100
changeset 41911 c6e66b32ce16
parent 34870 e10547372c41
child 42518 57367832b81a
permissions -rw-r--r--
adding lazysmallcheck example theory to HOL-ex session
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28909
40d87c73120d basic setup of .hgignore;
wenzelm
parents:
diff changeset
     1
syntax: glob
40d87c73120d basic setup of .hgignore;
wenzelm
parents:
diff changeset
     2
40d87c73120d basic setup of .hgignore;
wenzelm
parents:
diff changeset
     3
*~
28911
88193464e443 more .hgignore entries;
wenzelm
parents: 28909
diff changeset
     4
*.class
88193464e443 more .hgignore entries;
wenzelm
parents: 28909
diff changeset
     5
*.jar
28909
40d87c73120d basic setup of .hgignore;
wenzelm
parents:
diff changeset
     6
.DS_Store
40d87c73120d basic setup of .hgignore;
wenzelm
parents:
diff changeset
     7
40d87c73120d basic setup of .hgignore;
wenzelm
parents:
diff changeset
     8
40d87c73120d basic setup of .hgignore;
wenzelm
parents:
diff changeset
     9
syntax: regexp
40d87c73120d basic setup of .hgignore;
wenzelm
parents:
diff changeset
    10
31669
6802c34af5a9 ignore in-situ contrib symlinks
haftmann
parents: 28943
diff changeset
    11
^contrib
28909
40d87c73120d basic setup of .hgignore;
wenzelm
parents:
diff changeset
    12
^heaps/
40d87c73120d basic setup of .hgignore;
wenzelm
parents:
diff changeset
    13
^browser_info/
28943
9fb44eb4425d ignore aux stuff in doc-src;
wenzelm
parents: 28911
diff changeset
    14
^doc-src/.*\.aux
9fb44eb4425d ignore aux stuff in doc-src;
wenzelm
parents: 28911
diff changeset
    15
^doc-src/.*\.bbl
9fb44eb4425d ignore aux stuff in doc-src;
wenzelm
parents: 28911
diff changeset
    16
^doc-src/.*\.blg
9fb44eb4425d ignore aux stuff in doc-src;
wenzelm
parents: 28911
diff changeset
    17
^doc-src/.*\.dvi
9fb44eb4425d ignore aux stuff in doc-src;
wenzelm
parents: 28911
diff changeset
    18
^doc-src/.*\.idx
9fb44eb4425d ignore aux stuff in doc-src;
wenzelm
parents: 28911
diff changeset
    19
^doc-src/.*\.ind
31926
cdfe9a757d5f more hgignore;
wenzelm
parents: 31669
diff changeset
    20
^doc-src/.*\.lof
28943
9fb44eb4425d ignore aux stuff in doc-src;
wenzelm
parents: 28911
diff changeset
    21
^doc-src/.*\.log
9fb44eb4425d ignore aux stuff in doc-src;
wenzelm
parents: 28911
diff changeset
    22
^doc-src/.*\.out
9fb44eb4425d ignore aux stuff in doc-src;
wenzelm
parents: 28911
diff changeset
    23
^doc-src/.*\.rai
9fb44eb4425d ignore aux stuff in doc-src;
wenzelm
parents: 28911
diff changeset
    24
^doc-src/.*\.rao
9fb44eb4425d ignore aux stuff in doc-src;
wenzelm
parents: 28911
diff changeset
    25
^doc-src/.*\.toc
28909
40d87c73120d basic setup of .hgignore;
wenzelm
parents:
diff changeset
    26
34870
e10547372c41 ignore some src/Tools/jEdit stuff;
wenzelm
parents: 31926
diff changeset
    27
^src/Tools/jEdit/nbproject/private/
e10547372c41 ignore some src/Tools/jEdit stuff;
wenzelm
parents: 31926
diff changeset
    28
^src/Tools/jEdit/build/
e10547372c41 ignore some src/Tools/jEdit stuff;
wenzelm
parents: 31926
diff changeset
    29
^src/Tools/jEdit/dist/
e10547372c41 ignore some src/Tools/jEdit stuff;
wenzelm
parents: 31926
diff changeset
    30
^src/Tools/jEdit/contrib/