aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorDavid Aspinall1998-11-25 14:10:31 +0000
committerDavid Aspinall1998-11-25 14:10:31 +0000
commit3588aca7b6d5edebcde7a32e24d43531c35d85aa (patch)
treef1f2ba14f1f6457594ce97636cdbb683095d9201 /doc
parent73a59aba07146650d43fe3f7151114afa7d0c4be (diff)
Updated
Diffstat (limited to 'doc')
-rw-r--r--doc/.cvsignore21
1 files changed, 5 insertions, 16 deletions
diff --git a/doc/.cvsignore b/doc/.cvsignore
index 961dd664..145b4f15 100644
--- a/doc/.cvsignore
+++ b/doc/.cvsignore
@@ -14,20 +14,9 @@ ProofGeneral.info
ProofGeneral.cps
ProofGeneral.fns
ProofGeneral.vrs
-NewDoc.log
-NewDoc.dvi
-NewDoc.aux
-NewDoc.cp
-NewDoc.fn
-NewDoc.vr
-NewDoc.tp
-NewDoc.ky
-NewDoc.pg
-NewDoc.toc
-NewDoc.info
-NewDoc.cps
-NewDoc.fns
-NewDoc.vrs
-NewDoc.ps
-NewDoc.kys
+ProofGeneral.info-*
+
+
+
+