From 871a9e65009990963c12359531ea2beeacb7386d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Mon, 14 May 2018 18:29:02 +0200
Subject: gitlab: build sphinx doc in separate job

---
 Makefile.doc | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'Makefile.doc')

diff --git a/Makefile.doc b/Makefile.doc
index 4670c79ec..dde3a37b7 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -31,6 +31,7 @@ DVIPS:=dvips
 HTMLSTYLE:=coqremote
 
 # Sphinx-related variables
+SPHINXENV:=COQBIN="$(CURDIR)/bin/"
 SPHINXOPTS= -j4
 SPHINXBUILD= sphinx-build
 SPHINXBUILDDIR= doc/sphinx/_build
@@ -55,7 +56,7 @@ endif
 
 sphinx: $(SPHINX_DEPS)
 	$(SHOW)'SPHINXBUILD doc/sphinx'
-	$(HIDE)COQBIN="$(abspath bin)" $(SPHINXBUILD) -W -b html $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/html
+	$(HIDE)$(SPHINXENV) $(SPHINXBUILD) -W -b html $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/html
 	@echo
 	@echo "Build finished. The HTML pages are in $(SPHINXBUILDDIR)/html."
 
-- 
cgit v1.2.3