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/dune | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'doc/dune')

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