diff options
| author | Jim Fehrle | 2018-08-21 15:10:59 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2018-08-29 12:46:51 -0700 |
| commit | cc35d211ad7550d23d64828c177936990c08d681 (patch) | |
| tree | 34147c02b88d1e1bdd1d2687477776b98d9fa7e8 | |
| parent | bce734bfb2a118dbb487e5b88eba524ca14d2078 (diff) | |
Create SPHINXWARNERROR variable that controls whether the Sphinx
"treat errors as warnings" flag (-W) is applied. "1" or undefined
includes the flag, other values or undefined omit it.
Removed the "-warn-error" parameter to configure. "-profile XXX" will
no longer cause these flags to be used.
| -rw-r--r-- | Makefile.doc | 6 | ||||
| -rw-r--r-- | doc/README.md | 14 |
2 files changed, 18 insertions, 2 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." diff --git a/doc/README.md b/doc/README.md index 6c6e1f01fb..3e70bc443d 100644 --- a/doc/README.md +++ b/doc/README.md @@ -9,7 +9,7 @@ The Coq documentation includes The documentation of the latest released version is available on the Coq web site at [coq.inria.fr/documentation](http://coq.inria.fr/documentation). -Additionnally, you can view the documentation for the current master version at +Additionally, you can view the documentation for the current master version at <https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=documentation>. The reference manual is written is reStructuredText and compiled @@ -89,6 +89,18 @@ Alternatively, you can use some specific targets: Also note the `-with-doc yes` option of `./configure` to enable the build of the documentation as part of the default make target. +If you're editing Sphinx documentation, set SPHINXWARNERROR to 0 +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 SPINXWARNERROR=0` + +- ~~~ + export SPHINXWARNERROR=0 + ⋮ + make sphinx + ~~~ Installation ------------ |