aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-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