From 3d833269860ae9fe8e6f4a3d936d23404afe453e Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sun, 23 Dec 2018 17:37:28 +0100
Subject: [dune] Build refman with fatal warnings by default like in the
 Makefile build.

The way to override this default is not exactly the same as in the legacy Makefile
but it has been documented as well.
---
 doc/README.md | 27 +++++++++++++++------------
 doc/dune      |  6 ++++--
 2 files changed, 19 insertions(+), 14 deletions(-)

(limited to 'doc')

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)
-- 
cgit v1.2.3