aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorDavid Aspinall1999-06-28 14:05:50 +0000
committerDavid Aspinall1999-06-28 14:05:50 +0000
commita6b9bd585faed3976649d762dfda906a027ff4aa (patch)
tree2236dc2a9084724ecb24f9bd902dcfc9d350b57d /doc
parent9d29983323d2ca1b502d0ac4e8cf11c2f6225315 (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 ffdc0f67..0a134a47 100644
--- a/doc/.cvsignore
+++ b/doc/.cvsignore
@@ -15,6 +15,7 @@ ProofGeneral.cps
ProofGeneral.fns
ProofGeneral.vrs
ProofGeneral.info-*
+ProofGeneral.eps
ProofGeneral_*.html
ProofGeneral_toc.html
ProofGeneral_foot.html