1 files changed, 0 insertions, 22 deletions
diff --git a/proposals/check_index b/proposals/check_index
deleted file mode 100755
index 61db50d..0000000
--- a/proposals/check_index
+++ /dev/null
@@ -1,22 +0,0 @@
-#!/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/proposals"
-./reindex.py
-
-if ! git diff --quiet ; then
-    echo "Proposal index is not up-to-date. Run ./reindex.py to regenerate it." >&2
-    exit 1
-fi