Merge PR #9277: [dune] Build refman with fatal warnings like in the Makefile build.

2 files changed, 19 insertions, 14 deletions

diff --git a/doc/README.md b/doc/README.md
index 3db1261656..c41d269437 100644
--- a/doc/README.md
+++ b/doc/README.md
@@ -101,18 +101,21 @@ 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 refman SPHINXWARNERROR=0`
-
-- ~~~
-  export SPHINXWARNERROR=0
-    ⋮
-  make refman
-  ~~~
+To build the Sphinx documentation without stopping at the first
+warning with the legacy Makefile, set `SPHINXWARNERROR` to 0 as such:
+
+```
+SPHINXWARNERROR=0 make refman-html
+```
+
+To do the same with the Dune build system, change the value of the
+`SPHINXWARNOPT` variable (default is `-W`). The following will build
+the Sphinx documentation without stopping at the first warning, and
+store all the warnings in the file `/tmp/warn.log`:
+
+```
+SPHINXWARNOPT="-w/tmp/warn.log" dune build @refman-html
+```
 
 Installation
 ------------
diff --git a/doc/dune b/doc/dune
index 54ffa87205..6372fe4a91 100644
--- a/doc/dune
+++ b/doc/dune
@@ -10,8 +10,10 @@
   ;   + tools/coqdoc/coqdoc.css
   (package coq)
   (source_tree sphinx)
-  (source_tree tools))
- (action (run sphinx-build -j4 -b html -d sphinx_build/doctrees sphinx sphinx_build/html)))
+  (source_tree tools)
+  (env_var SPHINXWARNOPT))
+ (action
+  (run sphinx-build -j4 %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html)))
 
 (alias
  (name refman-html)