diff options
| -rwxr-xr-x | contrib/jenkins.sh | 5 |
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 |