Prefer make.sh for building docs as htmlhelp is removed from Makefile

* Also it's more flexible in locating necessary tools like sphinx-build or
  python
This commit is contained in:
baldurk
2018-08-18 16:44:05 +01:00
parent 92f593f38c
commit 5b89ababd5
+2 -2
View File
@@ -25,8 +25,8 @@ fi
# Step into the docs folder and build
pushd docs
make clean
make htmlhelp > /tmp/sphinx.log
./make.sh clean
./make.sh htmlhelp > /tmp/sphinx.log
if [ $? -ne 0 ]; then
$ERROR_SCRIPT /tmp/sphinx.log