isabelle: .hgignore@5bd30359e46e (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
56419 f47de9e82b0f ignore jedit mark files paulson <lp15@cam.ac.uk> parents: 55138 diff changeset	6	*.marks
48808 28f1d184c093 ignore some administrative files on newer Mercurial versions as well; wenzelm parents: 43287 diff changeset	7	*.orig
28f1d184c093 ignore some administrative files on newer Mercurial versions as well; wenzelm parents: 43287 diff changeset	8	*.rej
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/
64605 9c1173a7e4cb basic support for VSCode Language Server protocol; wenzelm parents: 63864 diff changeset	23	^src/Tools/VSCode/out/
9c1173a7e4cb basic support for VSCode Language Server protocol; wenzelm parents: 63864 diff changeset	24	^src/Tools/VSCode/extension/node_modules/
9c1173a7e4cb basic support for VSCode Language Server protocol; wenzelm parents: 63864 diff changeset	25	^src/Tools/VSCode/extension/protocol.log
63191 c3896c385c3e ignore Maven build products Lars Hupel <lars.hupel@mytum.de> parents: 56419 diff changeset	26	^Admin/jenkins/ci-extras/target/
63864 159882dbb339 ignore default output directory of 'build_stats' tool Lars Hupel <lars.hupel@mytum.de> parents: 63191 diff changeset	27	^stats/

author	haftmann
	Thu, 22 Dec 2016 08:43:30 +0100
changeset 64634	5bd30359e46e
parent 64605	9c1173a7e4cb
child 65744	92028ab1c3d7
permissions	-rw-r--r--