1 files changed, 22 insertions, 0 deletions
diff --git a/bin/check_index b/bin/check_index
new file mode 100755
index 0000000..a2e8c4f
--- /dev/null
+++ b/bin/check_index
@@ -0,0 +1,22 @@
+#!/usr/bin/env bash
+#
+# Give an error if somebody forgot to run ./reindex.py.
+#
+# Only works on a clean git checkout.
+
+set -e -u -o pipefail -x
+
+TOPLEVEL=$(dirname "$0")/..
+
+if ! git diff --quiet ; then
+    echo "Git repository is not clean. Cannot procede."
+    exit 2
+fi
+
+cd "$TOPLEVEL/"
+./bin/reindex
+
+if ! git diff --quiet ; then
+    echo "Proposal index is not up-to-date. Run ./reindex.py to regenerate it." >&2
+    exit 1
+fi