diff --git a/tools/jenkins/run_jenkins.sh b/tools/jenkins/run_jenkins.sh index 3fa5914bc11e9239c3ca5780126669207188eb77..a754015f4003fbcdbd5d52ebdb99bbbb87b048e7 100755 --- a/tools/jenkins/run_jenkins.sh +++ b/tools/jenkins/run_jenkins.sh @@ -44,7 +44,7 @@ then if [ "$ghprbPullId" != "" ] then # if we are building a pull request, grab corresponding refs. - FETCH_PULL_REQUEST_CMD="&& git fetch $GIT_URL +refs/pull/$ghprbPullId:refs/remotes/origin/pr/$ghprbPullId" + FETCH_PULL_REQUEST_CMD="&& git fetch $GIT_URL refs/pull/$ghprbPullId/merge refs/pull/$ghprbPullId/head" fi # Run tests inside docker