aboutsummaryrefslogtreecommitdiff
path: root/doc/dune
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-03-12 19:43:47 -0400
committerEmilio Jesus Gallego Arias2020-03-12 19:43:47 -0400
commit76d8a38a4591c604795c5429ffcbbe9daaa8945d (patch)
tree18d49d2ce24f1f19a5aa5c17ffc259ad8759d112 /doc/dune
parent1a7cdc1da9bff2e46acdd5c07a7eee5dcd27d731 (diff)
parentd1e0b777052bb94eff8226a57c40f0558308b10e (diff)
Merge PR #11796: Remove parallel building of Sphinx documentation.
Diffstat (limited to 'doc/dune')
-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)