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(-)

(limited to 'doc')

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