diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-14 18:29:02 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-08 23:27:08 +0200 |
| commit | 871a9e65009990963c12359531ea2beeacb7386d (patch) | |
| tree | 2726970832b00fbc7fa122ceda955d4995a508bd /Makefile.doc | |
| parent | 01128a2ff774f0ef249ee54a67e88d49ae254a4d (diff) | |
gitlab: build sphinx doc in separate job
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 3 |
1 files changed, 2 insertions, 1 deletions
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." |