aboutsummaryrefslogtreecommitdiff
path: root/doc/dune
diff options
context:
space:
mode:
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)