diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1998-09-16 15:32:05 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1998-09-16 15:32:05 +0000 |
| commit | b272e3a721cb82737bb350e4c4c1d28e63e8bb37 (patch) | |
| tree | 071d9e3f37fb341f6444862e758c4d14b0aa2d3c /doc/Makefile | |
| parent | 948364c897f7efbdf83c02b675f8717509cc839c (diff) | |
Makefile for building every kind of target from texi.
Diffstat (limited to 'doc/Makefile')
| -rw-r--r-- | doc/Makefile | 79 |
1 files changed, 79 insertions, 0 deletions
diff --git a/doc/Makefile b/doc/Makefile new file mode 100644 index 00000000..70be201e --- /dev/null +++ b/doc/Makefile @@ -0,0 +1,79 @@ +## +## Makefile for Proof General doc directory. +## +## Author: David Aspinall <da@dcs.ed.ac.uk> +## +## $Id$ +## +########################################################################### +## +## Use: +## make info,dvi,pdf,html - build respective docs from texi source. +## make doc - make all kinds of doc. +## +########################################################################### + +DOCNAME = ProofGeneral + +# program to make info files from .texi +MAKEINFO = makeinfo +# program to make dvi files from .texi +TEXI2DVI = texi2dvi +# program to make pdf files from .texi +TEXI2PDF = texi2pdf +# program to make html files from .texi +TEXI2HTML = texi2html + +.SUFFIXES: .texi .info .dvi .html .pdf + +.texi.info: + $(MAKEINFO) $< + +.texi.dvi: + $(TEXI2DVI) $< + +.texi.pdf: + $(TEXI2PDF) $< + +.texi.html: + $(TEXI2HTML) $< + + + +## +## doc : build info and dvi files from $(DOCNAME).texi +## +doc: dvi info + +## +## doc : build dvi, pdf, html, info +## +all: dvi pdf html info + +dvi: $(DOCNAME).dvi +pdf: $(DOCNAME).pdf +html: $(DOCNAME).html +info: $(DOCNAME).info + +# NB: for info, could make localdir automatically from +# START-INFO-DIR-ENTRY / END-INFO-DIR-ENTRY. +# Does some utility do this? + +## +## clean: Remove subsidiary documentation files +## +clean: + rm -f $(DOCNAME).?? $(DOCNAME).cps $(DOCNAME).cp0 + rm -f $(DOCNAME).aux $(DOCNAME).log $(DOCNAME).toc + rm -f *~ + +## +## distclean: Remove documentation targets +## +distclean: clean + rm -f $(DOCNAME).info* $(DOCNAME).dvi $(DOCNAME).pdf $(DOCNAME)*.html + + + + + |