diff options
Diffstat (limited to 'contrib')
| -rwxr-xr-x | contrib/update-pp.sh | 7 | ||||
| -rwxr-xr-x | contrib/update-tos.sh | 7 |
2 files changed, 14 insertions, 0 deletions
diff --git a/contrib/update-pp.sh b/contrib/update-pp.sh index 03aa237..89390a1 100755 --- a/contrib/update-pp.sh +++ b/contrib/update-pp.sh @@ -6,6 +6,13 @@ # Error checking on set -eu + +if ! htmlark --version >/dev/null; then + echo "htmlark not installed" + echo "Run 'pip install htmlark'" + exit 1 +fi + echo "Generating PP for ETag $VERSION" rm -f sphinx.log sphinx.err diff --git a/contrib/update-tos.sh b/contrib/update-tos.sh index 26d65ed..04fff48 100755 --- a/contrib/update-tos.sh +++ b/contrib/update-tos.sh @@ -6,6 +6,13 @@ # Error checking on set -eu + +if ! htmlark --version >/dev/null; then + echo "htmlark not installed" + echo "Run 'pip install htmlark'" + exit 1 +fi + echo "Generating TOS for ETag $VERSION" rm -f sphinx.log sphinx.err |