jenkins.sh: ensure $MAKE is set

Change-Id: I2da8acdfe3abf79f68db4d00d04a7d162f0123ce
2016-08-10 14:35:51 +02:00 · 2016-08-10 14:35:51 +02:00 · 0b4da058ad
parent 79cb245157
commit 0b4da058ad
1 changed files with 5 additions and 0 deletions
--- a/contrib/jenkins.sh
+++ b/contrib/jenkins.sh
@ -2,6 +2,11 @@

 set -ex

+if [ -z "$MAKE" ]; then
+  echo 'The $MAKE variable is not defined, cannot build'
+  exit 1
+fi
+
 if [ $sysmobts = "no" -a $sysmodsp = "yes" ]; then
   echo "This config does not make sense."
   exit 0