diff options
| author | Maxime Dénès | 2018-05-25 15:03:58 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-05-25 15:03:58 +0200 |
| commit | da49e86de39f8d9ed8709905e63cf442745a904f (patch) | |
| tree | fd8c359b0849c6ff8d8d03b4cd585a5cac10eaaf /Makefile.doc | |
| parent | d2533da244f770261478ae829167cb3a8ad38038 (diff) | |
| parent | 9811cda7698652b51e8ebdb25db7285ab8e5ae9a (diff) | |
Merge PR #7556: Add a setting to warn about empty object in the refman
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 41ae11b869..4670c79ece 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." |