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


From f6725356f22246fbf639ce59def6239905816ece Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 28 Apr 2020 20:41:07 +0200
Subject: [doc] [sphinx] Be silent when running latexmk

This is actually supported by Sphinx directly.
---
 doc/dune | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/dune b/doc/dune
index 80c4072541..c82e5a3df4 100644
--- a/doc/dune
+++ b/doc/dune
@@ -49,7 +49,7 @@
  (action
   (progn
    (run env COQLIB=%{project_root} sphinx-build -q %{env:SPHINXWARNOPT=-W} -b latex sphinx %{targets})
-   (chdir %{targets} (run make)))))
+   (chdir %{targets} (run make LATEXMKOPTS=-silent)))))
 
 ; Installable directories are not yet fully supported by Dune.  See
 ; ocaml/dune#1868.  Yet, this makes coq-doc.install a valid target to
-- 
cgit v1.2.3