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

1 files changed, 15 insertions, 12 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
 ------------