From bd4f3815eb3f6339f6f0a97894e8b1766df25ea0 Mon Sep 17 00:00:00 2001
From: Aidan Hobson Sayers <aidanhs@cantab.net>
Date: Fri, 7 Apr 2017 19:55:52 +0100
Subject: [PATCH] Disable errexit for sanity checking git repo

---
 src/ci/init_repo.sh | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/ci/init_repo.sh b/src/ci/init_repo.sh
index c235681cddd..633b88dd2c4 100755
--- a/src/ci/init_repo.sh
+++ b/src/ci/init_repo.sh
@@ -41,8 +41,10 @@ if [ ! -f "$cache_valid_file" ]; then
     rm -rf "$CACHE_DIR"
     mkdir "$CACHE_DIR"
 else
+    set +o errexit
     stat_lines=$(cd "$cache_src_dir" && git status --porcelain | wc -l)
-    stat_ec=$(cd "$cache_src_dir" && git status >/dev/null 2>&1 && echo $?)
+    stat_ec=$(cd "$cache_src_dir" && git status >/dev/null 2>&1; echo $?)
+    set -o errexit
     if [ ! -d "$cache_src_dir/.git" -o $stat_lines != 0 -o $stat_ec != 0 ]; then
         # Something is badly wrong - the cache valid file is here, but something
         # about the git repo is fishy. Nuke it all, just in case