Remove language file extension from bin/*

Putting ".sh" or ".py" on the end of scripts is an antipattern.
It makes it inconvenient to change the implementation language.

Change all call sites.

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