diff options
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 28 |
1 files changed, 19 insertions, 9 deletions
diff --git a/Makefile.doc b/Makefile.doc index 0dcf9daf27..db52607612 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -50,25 +50,35 @@ DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex ###################################################################### .PHONY: doc doc-html doc-pdf doc-ps -.PHONY: stdlib full-stdlib +.PHONY: stdlib full-stdlib sphinx -doc: sphinx stdlib +doc: refman stdlib ifndef QUICK SPHINX_DEPS := coq endif -sphinx: $(SPHINX_DEPS) - $(SHOW)'SPHINXBUILD doc/sphinx' - $(HIDE)$(SPHINXENV) $(SPHINXBUILD) -b html $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/html - @echo - @echo "Build finished. The HTML pages are in $(SPHINXBUILDDIR)/html." +# refman-html and refman-latex +refman-%: $(SPHINX_DEPS) + $(SHOW)'SPHINXBUILD doc/sphinx ($*)' + $(HIDE)$(SPHINXENV) $(SPHINXBUILD) -b $* \ + $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/$* + +refman-pdf: refman-latex + +$(MAKE) -C $(SPHINXBUILDDIR)/latex + +refman: $(SPHINX_DEPS) + +$(MAKE) refman-html + +$(MAKE) refman-pdf + +# compatibility alias +sphinx: refman-html doc-html:\ - doc/stdlib/html/index.html sphinx + doc/stdlib/html/index.html refman-html doc-pdf:\ - doc/stdlib/Library.pdf + doc/stdlib/Library.pdf refman-pdf doc-ps:\ doc/stdlib/Library.ps |