From 03ce3fc9ef0bb85d43bb5351b5d109bd0d6743c1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 28 Apr 2020 17:41:18 +0200
Subject: [doc] [sphinx] Run in silent mode by default

The convention in the dune build is to be silent except for warnings
and errors, so they don't go unnoticed.

We could have this controlled by a variable if needed (likely would
require some support from Dune?)

Solves part of #12194
---
 doc/dune | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/dune b/doc/dune
index 8b005f5b2f..80c4072541 100644
--- a/doc/dune
+++ b/doc/dune
@@ -32,7 +32,7 @@
   unreleased.rst
   (env_var SPHINXWARNOPT))
  (action
-  (run env COQLIB=%{project_root} sphinx-build %{env:SPHINXWARNOPT=-W} -b html sphinx %{targets})))
+  (run env COQLIB=%{project_root} sphinx-build -q %{env:SPHINXWARNOPT=-W} -b html sphinx %{targets})))
 
 (rule
  (targets refman-pdf)
@@ -48,7 +48,7 @@
   (env_var SPHINXWARNOPT))
  (action
   (progn
-   (run env COQLIB=%{project_root} sphinx-build %{env:SPHINXWARNOPT=-W} -b latex sphinx %{targets})
+   (run env COQLIB=%{project_root} sphinx-build -q %{env:SPHINXWARNOPT=-W} -b latex sphinx %{targets})
    (chdir %{targets} (run make)))))
 
 ; Installable directories are not yet fully supported by Dune.  See
-- 
cgit v1.2.3