diff options
| author |  Clément Pit-Claudel <clement.pitclaudel@live.com> | 2018-05-13 12:07:21 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel <clement.pitclaudel@live.com> | 2018-05-22 11:40:13 -0400 |
| commit | 3ae50f0ba006e77e27fbe81b192234de1ee617c5 (patch) | |
| tree | 4600cc2c93af3503a081f08fee9e23a3247b87e1 /Makefile.doc | |
| parent | 35d27dfd9df0cf94b1218812bc6c1e2bc832ec1d (diff) | |
[doc] Fix an incorrect use of $PWD in Makefile.doc
Diffstat (limited to 'Makefile.doc')
| -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." |