From bad10f7fed982584c8e2850c06ce71a0ab24966f Mon Sep 17 00:00:00 2001 From: Alex J Best Date: Tue, 10 Oct 2023 12:08:39 +0200 Subject: [PATCH] Use as many jobs as you have cores to build docs --- doc/Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/Makefile b/doc/Makefile index bc9dc0769a..d685e40ed1 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -2,7 +2,7 @@ # # You can set these variables from the command line. -SPHINXOPTS = +SPHINXOPTS = -j=auto SPHINXBUILD = sphinx-build SPHINXPROJ = Flint SOURCEDIR = source @@ -17,4 +17,4 @@ help: # Catch-all target: route all unknown targets to Sphinx using the new # "make mode" option. $(O) is meant as a shortcut for $(SPHINXOPTS). %: Makefile - @$(SPHINXBUILD) -M $@ "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O) \ No newline at end of file + @$(SPHINXBUILD) -M $@ "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)