From 3ae50f0ba006e77e27fbe81b192234de1ee617c5 Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel <clement.pitclaudel@live.com>
Date: Sun, 13 May 2018 12:07:21 -0400
Subject: [doc] Fix an incorrect use of $PWD in Makefile.doc

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

(limited to 'Makefile.doc')

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."
 
-- 
cgit v1.2.3