1 files changed, 15 insertions, 0 deletions
diff --git a/build_html.sh b/build_html.sh
new file mode 100755
index 0000000..ae78080
--- /dev/null
+++ b/build_html.sh
@@ -0,0 +1,15 @@
+#!/usr/bin/env bash
+
+set -e -u -o pipefail
+
+TOPLEVEL=$(realpath $(dirname "$0"))
+cd "${TOPLEVEL}/proposals"
+./reindex.py
+
+cd "${TOPLEVEL}/mdbook/spec"
+mdbook build
+
+cd "${TOPLEVEL}/mdbook/proposals"
+mdbook build
+
+