isabelle: .hgignore@bf49b7a85936 (annotated)

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/

author	wenzelm
	Sun, 13 Feb 2011 17:45:21 +0100
changeset 41760	bf49b7a85936
parent 34870	e10547372c41
child 42518	57367832b81a
permissions	-rw-r--r--