diff options
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/Makefile.doc b/Makefile.doc index d13d0c09e3..4670c79ece 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -49,9 +49,13 @@ DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex doc: sphinx stdlib -sphinx: coq +ifndef QUICK +SPHINX_DEPS := coq +endif + +sphinx: $(SPHINX_DEPS) $(SHOW)'SPHINXBUILD doc/sphinx' - $(HIDE)COQBIN="$(PWD)/bin" $(SPHINXBUILD) -W -b html $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/html + $(HIDE)COQBIN="$(abspath bin)" $(SPHINXBUILD) -W -b html $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/html @echo @echo "Build finished. The HTML pages are in $(SPHINXBUILDDIR)/html." |