diff --git a/docker/launch-jenkins.sh b/docker/launch-jenkins.sh old mode 100644 new mode 100755 index 0a366df65dcf2d5dba05dc6dac4a51cf7f53642f..64dc1ec73f68e621cdd737595983b6b9a217f6fe --- a/docker/launch-jenkins.sh +++ b/docker/launch-jenkins.sh @@ -2,11 +2,11 @@ # defaults, can be overriden by environment variables # user to run Jenkins as -- see NOTE below regarding Docker access permissions -JENKINS_USER ?= jenkins +: ${JENKINS_USER=jenkins} # port for Jenkins on host machine -JENKINS_PORT ?= 8080 +: ${JENKINS_PORT=8080} # make Jenkins config persistent by mounting into this folder -JENKINS_HOME ?= $(pwd)/jenkins_home +: ${JENKINS_HOME=$(pwd)/jenkins_home} mkdir -p $JENKINS_HOME