diff options
| author | Emilio Jesus Gallego Arias | 2020-04-28 20:41:07 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-28 20:48:44 +0200 |
| commit | f6725356f22246fbf639ce59def6239905816ece (patch) | |
| tree | 652386e03b0f481aba025a53e391fdf0df4aca32 /doc/dune | |
| parent | 03ce3fc9ef0bb85d43bb5351b5d109bd0d6743c1 (diff) | |
[doc] [sphinx] Be silent when running latexmk
This is actually supported by Sphinx directly.
Diffstat (limited to 'doc/dune')
| -rw-r--r-- | doc/dune | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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 |