diff options
| author |  Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-12-14 14:49:29 +0000 |
|---|---|---|
| committer | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-12-14 14:49:29 +0000 |
| commit | 25e823e27199b92d0a8ac7ee445c61d91a647ab0 (patch) | |
| tree | 5eccdc44ea79aa84e55906c331d9e23ccc89c273 /doc/Makefile | |
| parent | 6f92823397844051832a9e82c6e38005f2a2c62e (diff) | |
rearrange pages automatically
Diffstat (limited to 'doc/Makefile')
| -rw-r--r-- | doc/Makefile | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/doc/Makefile b/doc/Makefile index 7401acfe..3ecfb7d9 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -19,6 +19,18 @@ DOCNAME = ProofGeneral MAKEINFO = makeinfo TEXI2DVI = texi2dvi + +DVICONCAT = dviconcat +DVISELECT = dviselect + +# Assumes actual first two pages belong to titlepage +TITLERANGE = =1,=2 + +# Assumes that main document starts on third actual page +MAINRANGE = =3,=4,5: + +TOC = :_1 + DVI2PS = dvips TEXI2PDF = texi2pdf TEXI2HTML = texi2html @@ -30,7 +42,12 @@ EMACS = xemacs -batch $(MAKEINFO) $< .texi.dvi: - $(TEXI2DVI) $< + $(TEXI2DVI) $< + $(DVISELECT) -i $*.dvi -o $*.tmp1 $(TITLERANGE) + $(DVISELECT) -i $*.dvi -o $*.tmp2 $(MAINRANGE) + $(DVISELECT) -i $*.dvi -o $*.tmp3 $(TOC) + $(DVICONCAT) -o $*.dvi $*.tmp1 $*.tmp3 $*.tmp2 + rm -f $*.tmp1 $*.tmp2 $*.tmp3 .texi.pdf: |