From 437ff7c3f0f36d9832731746f6113a0bbd435a1b Mon Sep 17 00:00:00 2001
From: =?utf8?q?Michael=20P=C3=B6hn?= <michael.poehn@fsfe.org>
Date: Fri, 24 Mar 2017 00:49:02 +0100
Subject: [PATCH] jenkins makebuildserver fail if vagrant box was not created

---
 jenkins-build-makebuildserver | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/jenkins-build-makebuildserver b/jenkins-build-makebuildserver
index 15363f1a..ff3104f7 100755
--- a/jenkins-build-makebuildserver
+++ b/jenkins-build-makebuildserver
@@ -54,6 +54,12 @@ echo "apt_package_cache = True" >> $WORKSPACE/makebuildserver.config.py
 echo "copy_caches_from_host = True" >> $WORKSPACE/makebuildserver.config.py
 ./makebuildserver --verbose --clean
 
+if [ -z "`vagrant box list | egrep '^buildserver\s+\((libvirt|virtualbox), [0-9]+\)$'`" ]; then
+    vagrant box list
+    echo "ERROR: buildserver box does not exist!"
+    exit 1
+fi
+
 # this can be handled in the jenkins job, or here:
 if [ -e fdroiddata ]; then
     cd fdroiddata
@@ -73,7 +79,7 @@ if [ -z $ANDROID_HOME ]; then
         . ~/.android/bashrc
     else
         echo "ANDROID_HOME must be set!"
-        exit
+        exit 1
     fi
 fi
 
-- 
2.30.2