diff --git a/docs/build.sh b/docs/build.sh new file mode 100755 index 000000000..d9c0428ad --- /dev/null +++ b/docs/build.sh @@ -0,0 +1,20 @@ +#!/bin/sh + +# usage: +# ./build.sh +# ./build.sh sphinx-executable +# JOBS=3 ./build.sh ... + +cd $(dirname "$0") +cd .. + +sphinx=sphinx-build +if [ -n "$1" ]; then + sphinx=$1 +fi + +if [ -z "$JOBS" ]; then + JOBS=2 +fi + +"$sphinx" -a -E -q -b html . ./docs/html -w ./docs/_sphinx-warnings.txt -j "$JOBS"