aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorJim Fehrle2018-08-21 15:10:59 -0700
committerJim Fehrle2018-08-29 12:46:51 -0700
commitcc35d211ad7550d23d64828c177936990c08d681 (patch)
tree34147c02b88d1e1bdd1d2687477776b98d9fa7e8 /doc
parentbce734bfb2a118dbb487e5b88eba524ca14d2078 (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.
Diffstat (limited to 'doc')
-rw-r--r--doc/README.md14
1 files changed, 13 insertions, 1 deletions
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
------------