diff options
| -rw-r--r-- | Makefile.doc | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.doc b/Makefile.doc index 41ae11b86..4670c79ec 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -55,7 +55,7 @@ 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." |