aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorThéo Zimmermann2020-03-10 16:39:50 +0100
committerThéo Zimmermann2020-03-10 16:39:50 +0100
commitd1e0b777052bb94eff8226a57c40f0558308b10e (patch)
treef91252e8b6588e395a7dbbf84bae0814195c1ab9
parent3a5469b2097c55ecf952ead470caf03b6112cd9e (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/dune2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/dune b/doc/dune
index 3a8efbb36d..02ca33b682 100644
--- a/doc/dune
+++ b/doc/dune
@@ -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)