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.

1 files changed, 17 insertions, 0 deletions

diff --git a/bin/build_html b/bin/build_html
new file mode 100755
index 0000000..026c525
--- /dev/null
+++ b/bin/build_html
@@ -0,0 +1,17 @@
+#!/usr/bin/env bash
+
+set -e -u -o pipefail -x
+
+: ${MDBOOK:=mdbook}
+
+TOPLEVEL=$(realpath $(dirname "$0"))/..
+cd "${TOPLEVEL}"
+./bin/reindex
+
+./bin/make_redirects
+
+cd "${TOPLEVEL}/mdbook/spec"
+$MDBOOK build
+
+cd "${TOPLEVEL}/mdbook/proposals"
+$MDBOOK build