diff options
| -rw-r--r-- | .gitlab-ci.yml | 2 | ||||
| -rw-r--r-- | Makefile.doc | 27 | ||||
| -rw-r--r-- | doc/README.md | 11 |
3 files changed, 23 insertions, 17 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 15fcdf371a..1fb44ccbbe 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -112,7 +112,7 @@ after_script: - not-a-real-job script: - SPHINXENV='COQBIN="'"$PWD"'/_install_ci/bin/" COQBOOT=no' - - make -j "$NJOBS" SPHINXENV="$SPHINXENV" SPHINX_DEPS= sphinx + - make -j "$NJOBS" SPHINXENV="$SPHINXENV" SPHINX_DEPS= refman - make install-doc-sphinx artifacts: name: "$CI_JOB_NAME" 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);\ diff --git a/doc/README.md b/doc/README.md index 1461fa2e2c..3db1261656 100644 --- a/doc/README.md +++ b/doc/README.md @@ -88,8 +88,11 @@ Alternatively, you can use some specific targets: - `make doc-html` to produce all HTML documents -- `make sphinx` - to produce the HTML and PDF versions of the reference manual +- `make refman` + to produce the HTML and PDF versions of the reference manual + +- `make refman-{html,pdf}` + to produce only one format of the reference manual - `make stdlib` to produce all formats of the Coq standard library @@ -103,12 +106,12 @@ to avoid treating Sphinx warnings as errors. Otherwise, Sphinx quits upon detecting the first warning. You can set this on the Sphinx `make` command line or as an environment variable: -- `make sphinx SPHINXWARNERROR=0` +- `make refman SPHINXWARNERROR=0` - ~~~ export SPHINXWARNERROR=0 ⋮ - make sphinx + make refman ~~~ Installation |