diff options
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 27 |
1 files changed, 15 insertions, 12 deletions
diff --git a/Makefile.doc b/Makefile.doc index 788e4e61e7..db52607612 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -50,32 +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-html and sphinx-latex -sphinx-%: $(SPHINX_DEPS) +# refman-html and refman-latex +refman-%: $(SPHINX_DEPS) $(SHOW)'SPHINXBUILD doc/sphinx ($*)' $(HIDE)$(SPHINXENV) $(SPHINXBUILD) -b $* \ $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/$* -sphinx-pdf: sphinx-latex +refman-pdf: refman-latex +$(MAKE) -C $(SPHINXBUILDDIR)/latex -sphinx: $(SPHINX_DEPS) - +$(MAKE) sphinx-html - +$(MAKE) sphinx-pdf +refman: $(SPHINX_DEPS) + +$(MAKE) refman-html + +$(MAKE) refman-pdf + +# compatibility alias +sphinx: refman-html doc-html:\ - doc/stdlib/html/index.html sphinx-html + doc/stdlib/html/index.html refman-html doc-pdf:\ - doc/stdlib/Library.pdf sphinx-pdf + doc/stdlib/Library.pdf refman-pdf doc-ps:\ doc/stdlib/Library.ps @@ -188,7 +191,7 @@ install-doc-meta: $(MKDIR) $(FULLDOCDIR) $(INSTALLLIB) doc/LICENSE $(FULLDOCDIR)/LICENSE.doc -install-doc-html: install-doc-stdlib-html install-doc-sphinx-html +install-doc-html: install-doc-stdlib-html install-doc-sphinx install-doc-stdlib-html: $(MKDIR) $(FULLDOCDIR)/html/stdlib @@ -199,7 +202,7 @@ install-doc-printable: $(INSTALLLIB) doc/stdlib/Library.pdf $(FULLDOCDIR)/pdf $(INSTALLLIB) doc/stdlib/Library.ps $(FULLDOCDIR)/ps -install-doc-sphinx-html: +install-doc-sphinx: $(MKDIR) $(FULLDOCDIR)/sphinx (for f in `cd doc/sphinx/_build; find . -type f`; do \ $(MKDIR) $$(dirname $(FULLDOCDIR)/sphinx/$$f);\ |