diff options
| author | Emilio Jesus Gallego Arias | 2020-04-28 17:41:18 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-28 20:48:18 +0200 |
| commit | 03ce3fc9ef0bb85d43bb5351b5d109bd0d6743c1 (patch) | |
| tree | 006154f8629d1b12a002c280e2b9a83aae3d05e1 | |
| parent | 16559843925f3489b61920ff398680f10f1f00cc (diff) | |
[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
| -rw-r--r-- | doc/dune | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -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 |