diff options
| author | Théo Zimmermann | 2018-08-30 09:59:14 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-08-30 09:59:14 +0200 |
| commit | 0745b31e986b79692e4e282877555963d0f26a8f (patch) | |
| tree | cfa8b67d68f2e75343f1b8647509ce8f22ae5662 /Makefile.doc | |
| parent | 831d899ef214c55fb8fb50c804ea4d9da3b63d65 (diff) | |
| parent | cc35d211ad7550d23d64828c177936990c08d681 (diff) | |
Merge PR #8292: Create SPHINXWARNERROR variable to control Sphinx "warn as error" argument in make
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/Makefile.doc b/Makefile.doc index dde3a37b70..1b1198c1f2 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -33,6 +33,10 @@ HTMLSTYLE:=coqremote # Sphinx-related variables SPHINXENV:=COQBIN="$(CURDIR)/bin/" SPHINXOPTS= -j4 +SPHINXWARNERROR ?= 1 +ifeq ($(SPHINXWARNERROR),1) +SPHINXOPTS += -W +endif SPHINXBUILD= sphinx-build SPHINXBUILDDIR= doc/sphinx/_build @@ -56,7 +60,7 @@ endif sphinx: $(SPHINX_DEPS) $(SHOW)'SPHINXBUILD doc/sphinx' - $(HIDE)$(SPHINXENV) $(SPHINXBUILD) -W -b html $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/html + $(HIDE)$(SPHINXENV) $(SPHINXBUILD) -b html $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/html @echo @echo "Build finished. The HTML pages are in $(SPHINXBUILDDIR)/html." |