aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1998-10-15 14:29:24 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1998-10-15 14:29:24 +0000
commit3259b182e3726d5a31e35489ad41f7fc747c32f3 (patch)
treebe45e7f84fb574181d9f501d13ad9af7b9d2e941
parentebd3b16b3f00ff8fc7efc05e0fe5a37476bddbc8 (diff)
Added .ignore for documentation targets and intermediates.
-rw-r--r--doc/.cvsignore14
1 files changed, 14 insertions, 0 deletions
diff --git a/doc/.cvsignore b/doc/.cvsignore
new file mode 100644
index 00000000..3e902e63
--- /dev/null
+++ b/doc/.cvsignore
@@ -0,0 +1,14 @@
+ProofGeneral.log
+ProofGeneral.dvi
+ProofGeneral.aux
+ProofGeneral.cp
+ProofGeneral.fn
+ProofGeneral.vr
+ProofGeneral.tp
+ProofGeneral.ky
+ProofGeneral.pg
+ProofGeneral.toc
+ProofGeneral.info
+ProofGeneral.cps
+ProofGeneral.fns
+ProofGeneral.vrs \ No newline at end of file