1 files changed, 1 insertions, 0 deletions
diff --git a/push-script/push.sh b/push-script/push.sh
index b043fbe..94a2a99 100755
--- a/push-script/push.sh
+++ b/push-script/push.sh
@@ -105,6 +105,7 @@ for id in $COMMIT_IDS; do
   SPACES=`make --quiet check-spaces`;
   if [ "$SPACES" != "" ]; then
     make check-spaces;
+    exit 1;
   fi
   # Disabled because it takes forever.
   #make distcheck $MAKE_ARGS;