aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorNeels Hofmeyr <neels@hofmeyr.de>2016-08-10 14:35:51 +0200
committerNeels Hofmeyr <nhofmeyr@sysmocom.de>2016-08-11 11:06:26 +0000
commit0b4da058ad45984904c6860ec3820b213c683cce (patch)
tree215d309d57df33a1361f53d88713c36e8b2797a0
parent79cb2451576ff07fa65a819f605c82e732120e4c (diff)
jenkins.sh: ensure $MAKE is set
-rwxr-xr-xcontrib/jenkins.sh5
1 files changed, 5 insertions, 0 deletions
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