From cc35d211ad7550d23d64828c177936990c08d681 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Tue, 21 Aug 2018 15:10:59 -0700
Subject: 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.
---
 Makefile.doc  |  6 +++++-
 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
 ------------
-- 
cgit v1.2.3