diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/.cvsignore | 1 | ||||
| -rw-r--r-- | doc/Makefile | 4 |
2 files changed, 3 insertions, 2 deletions
diff --git a/doc/.cvsignore b/doc/.cvsignore index ebf58016..5966f115 100644 --- a/doc/.cvsignore +++ b/doc/.cvsignore @@ -17,6 +17,7 @@ ProofGeneral.fns ProofGeneral.vrs ProofGeneral.info-* ProofGeneral.eps +ProofGeneral.txt ProofGeneral_*.html ProofGeneral_toc.html ProofGeneral_foot.html diff --git a/doc/Makefile b/doc/Makefile index f89d92df..d136277d 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -33,7 +33,7 @@ TOC = :_1 DVI2PS = dvips TEXI2PDF = texi2pdf -TEXI2HTML = texi2html +TEXI2HTML = texi2html -expandinfo -number -split_chapter EMACS = xemacs -batch .SUFFIXES: .texi .info .dvi .html .pdf .ps .eps .tiff .gz @@ -59,7 +59,7 @@ EMACS = xemacs -batch $(DVI2PS) $< -o $*.ps .texi.html: - $(TEXI2HTML) -expandinfo -split_chapter $< + $(TEXI2HTML) $< default: doc |