From 0b4da058ad45984904c6860ec3820b213c683cce Mon Sep 17 00:00:00 2001
From: Neels Hofmeyr <neels@hofmeyr.de>
Date: Wed, 10 Aug 2016 14:35:51 +0200
Subject: jenkins.sh: ensure $MAKE is set

Change-Id: I2da8acdfe3abf79f68db4d00d04a7d162f0123ce
---
 contrib/jenkins.sh | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/contrib/jenkins.sh b/contrib/jenkins.sh
index 27cdaa99..7d3acc07 100755
--- 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
-- 
cgit v1.2.3