diff options
Diffstat (limited to 'bin')
-rwxr-xr-x | bin/build_html (renamed from bin/build_html.sh) | 4 | ||||
-rwxr-xr-x | bin/check_index | 2 | ||||
-rwxr-xr-x | bin/make_redirects (renamed from bin/make_redirects.py) | 0 | ||||
-rwxr-xr-x | bin/reindex (renamed from bin/reindex.py) | 0 |
4 files changed, 3 insertions, 3 deletions
diff --git a/bin/build_html.sh b/bin/build_html index 09b92e2..026c525 100755 --- a/bin/build_html.sh +++ b/bin/build_html @@ -6,9 +6,9 @@ set -e -u -o pipefail -x TOPLEVEL=$(realpath $(dirname "$0"))/.. cd "${TOPLEVEL}" -./bin/reindex.py +./bin/reindex -./bin/make_redirects.py +./bin/make_redirects cd "${TOPLEVEL}/mdbook/spec" $MDBOOK build diff --git a/bin/check_index b/bin/check_index index 77bdb02..a2e8c4f 100755 --- a/bin/check_index +++ b/bin/check_index @@ -14,7 +14,7 @@ if ! git diff --quiet ; then fi cd "$TOPLEVEL/" -./bin/reindex.py +./bin/reindex if ! git diff --quiet ; then echo "Proposal index is not up-to-date. Run ./reindex.py to regenerate it." >&2 diff --git a/bin/make_redirects.py b/bin/make_redirects index ea8ea3b..ea8ea3b 100755 --- a/bin/make_redirects.py +++ b/bin/make_redirects diff --git a/bin/reindex.py b/bin/reindex index 57ac403..57ac403 100755 --- a/bin/reindex.py +++ b/bin/reindex |