aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorDavid Aspinall1999-06-28 18:11:05 +0000
committerDavid Aspinall1999-06-28 18:11:05 +0000
commitda3ff0ce04613752aac7559ba6d12bc884d76340 (patch)
treee2dfcfc1c6a2a832c2778d3446a5019f529219c7 /doc
parentac8098524252b459416fff7761010e901d1fe223 (diff)
Updated.
Diffstat (limited to 'doc')
-rw-r--r--doc/.cvsignore1
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/.cvsignore b/doc/.cvsignore
index 0a134a47..ebf58016 100644
--- a/doc/.cvsignore
+++ b/doc/.cvsignore
@@ -1,6 +1,7 @@
ProofGeneral.log
ProofGeneral.dvi
ProofGeneral.ps
+ProofGeneral.ps.gz
ProofGeneral.kys
ProofGeneral.aux
ProofGeneral.cp