diff options
Diffstat (limited to 'bin')
| -rwxr-xr-x | bin/build_html.sh | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/bin/build_html.sh b/bin/build_html.sh index 56b8b93..09b92e2 100755 --- a/bin/build_html.sh +++ b/bin/build_html.sh @@ -2,6 +2,8 @@ set -e -u -o pipefail -x +: ${MDBOOK:=mdbook} + TOPLEVEL=$(realpath $(dirname "$0"))/.. cd "${TOPLEVEL}" ./bin/reindex.py @@ -9,7 +11,7 @@ cd "${TOPLEVEL}" ./bin/make_redirects.py cd "${TOPLEVEL}/mdbook/spec" -mdbook build +$MDBOOK build cd "${TOPLEVEL}/mdbook/proposals" -mdbook build +$MDBOOK build |