isabelle: .hgignore@bab6cade3cc5 (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
48808 28f1d184c093 ignore some administrative files on newer Mercurial versions as well; wenzelm parents: 43287 diff changeset	6	*.orig
28f1d184c093 ignore some administrative files on newer Mercurial versions as well; wenzelm parents: 43287 diff changeset	7	*.rej
54582 cb17feba74e0 MaSH files should be ignored paulson parents: 54560 diff changeset	8	*.pyc
28909 40d87c73120d basic setup of .hgignore; wenzelm parents: diff changeset	9	.DS_Store
54560 7f36da77130d more .hgignore; wenzelm parents: 48973 diff changeset	10	.swp
28909 40d87c73120d basic setup of .hgignore; wenzelm parents: diff changeset	11
40d87c73120d basic setup of .hgignore; wenzelm parents: diff changeset	12
40d87c73120d basic setup of .hgignore; wenzelm parents: diff changeset	13	syntax: regexp
40d87c73120d basic setup of .hgignore; wenzelm parents: diff changeset	14
31669 6802c34af5a9 ignore in-situ contrib symlinks haftmann parents: 28943 diff changeset	15	^contrib
28909 40d87c73120d basic setup of .hgignore; wenzelm parents: diff changeset	16	^heaps/
40d87c73120d basic setup of .hgignore; wenzelm parents: diff changeset	17	^browser_info/
48973 fcd21f714996 updated .hgignore to reflect to (almost) clean result of build_doc; wenzelm parents: 48808 diff changeset	18	^doc/.*\.dvi
fcd21f714996 updated .hgignore to reflect to (almost) clean result of build_doc; wenzelm parents: 48808 diff changeset	19	^doc/.*\.eps
fcd21f714996 updated .hgignore to reflect to (almost) clean result of build_doc; wenzelm parents: 48808 diff changeset	20	^doc/.*\.pdf
fcd21f714996 updated .hgignore to reflect to (almost) clean result of build_doc; wenzelm parents: 48808 diff changeset	21	^doc/.*\.ps
43287 acc680ab6204 simplified directory structure; wenzelm parents: 43281 diff changeset	22	^src/Tools/jEdit/dist/

author	haftmann
	Fri, 27 Dec 2013 14:35:14 +0100
changeset 54868	bab6cade3cc5
parent 54582	cb17feba74e0
child 55138	2fa86fa27a0f
permissions	-rw-r--r--