From 6ee44b62d0a858a2c298c9cdfefe29c583d51a00 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 10 Mar 2020 08:56:05 +0100
Subject: Disable parallel build of Sphinx documentation

We are using some Sphinx extensions that are not safe w.r.t. parallel
reaading.
---
 Makefile.doc | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Makefile.doc b/Makefile.doc
index 1249555cd7..5aa1ae9850 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -38,10 +38,11 @@ SPHINXENV:=COQBIN="$(CURDIR)/bin/" COQLIB="$(WIN_CURDIR)"
 else
 SPHINXENV:=COQBIN="$(CURDIR)/bin/" COQLIB="$(CURDIR)"
 endif
-SPHINXOPTS= -j4
 SPHINXWARNERROR ?= 1
 ifeq ($(SPHINXWARNERROR),1)
-SPHINXOPTS += -W
+SPHINXOPTS= -W
+else
+SPHINXOPTS=
 endif
 SPHINXBUILD= sphinx-build
 SPHINXBUILDDIR= doc/sphinx/_build
-- 
cgit v1.2.3