diff options
| author | Théo Zimmermann | 2020-03-10 16:39:50 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-03-10 16:39:50 +0100 |
| commit | d1e0b777052bb94eff8226a57c40f0558308b10e (patch) | |
| tree | f91252e8b6588e395a7dbbf84bae0814195c1ab9 | |
| parent | 3a5469b2097c55ecf952ead470caf03b6112cd9e (diff) | |
Remove parallel building of Sphinx documentation.
Since version 1.0.0 of the sphinxcontrib-bibtex extension, parallel
building of the Sphinx documentation emits a warning (and thus makes
our warning-free build fail).
This change was already done in Makefile.doc as part of #11732.
| -rw-r--r-- | doc/dune | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -14,7 +14,7 @@ unreleased.rst (env_var SPHINXWARNOPT)) (action - (run env COQLIB=%{project_root} sphinx-build -j4 %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) + (run env COQLIB=%{project_root} sphinx-build %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) (alias (name refman-html) |
