From: Michael Pöhn <michael.poehn@fsfe.org>
Date: Thu, 23 Mar 2017 23:49:02 +0000 (+0100)
Subject: jenkins makebuildserver fail if vagrant box was not created
X-Git-Tag: 0.8~56^2~36
X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ianmdlvl/git?a=commitdiff_plain;h=437ff7c3f0f36d9832731746f6113a0bbd435a1b;p=fdroidserver.git

jenkins makebuildserver fail if vagrant box was not created
---

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