aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2007-06-19 12:16:42 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2007-06-19 12:16:42 +0000
commited4cb92674704fac386cbe418397ee7e78c1adb7 (patch)
treed7f0d11b2d4d310651f5b871d853143f4c693137 /doc
parent762d5e9326ed02c0505e37b6b957511eef123b40 (diff)
New subdirs for html
Diffstat (limited to 'doc')
-rw-r--r--doc/.cvsignore6
1 files changed, 2 insertions, 4 deletions
diff --git a/doc/.cvsignore b/doc/.cvsignore
index 6a126a00..c667379c 100644
--- a/doc/.cvsignore
+++ b/doc/.cvsignore
@@ -18,10 +18,8 @@ ProofGeneral.fns
ProofGeneral.vrs
ProofGeneral.info-*
ProofGeneral.txt
-ProofGeneral_*.html
-ProofGeneral_toc.html
-ProofGeneral_foot.html
-PG-adapting.log
+ProofGeneral
+PG-adapting
PG-adapting.dvi
PG-adapting.ps
PG-adapting.pdf