diff options
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/jenkins/run_jenkins.sh | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/tools/jenkins/run_jenkins.sh b/tools/jenkins/run_jenkins.sh index f2091e2423..3ac2e5441e 100755 --- a/tools/jenkins/run_jenkins.sh +++ b/tools/jenkins/run_jenkins.sh @@ -51,11 +51,8 @@ then # Make sure docker image has been built. Should be instantaneous if so. docker build -t $DOCKER_IMAGE_NAME tools/jenkins/grpc_jenkins_slave - if [ "$ghprbPullId" != "" ] - then - # if we are building a pull request, grab corresponding refs. - FETCH_PULL_REQUEST_CMD="&& git fetch $GIT_URL refs/pull/$ghprbPullId/merge refs/pull/$ghprbPullId/head" - fi + # Create a local branch so the child Docker script won't complain + git branch jenkins-docker # Make sure the CID file is gone. rm -f docker.cid |