diff --git a/Jenkinsfile2 b/Jenkinsfile2 index bc309ff66ce6da198aea934c10ddecc2461a746b..d7df07f06afd8e1e483455e3ce925a03f28740fd 100644 --- a/Jenkinsfile2 +++ b/Jenkinsfile2 @@ -53,6 +53,7 @@ def check_docs() { } sh ''' cd ${WKC} + git remote prune origin git pull >/dev/null git fetch origin +refs/pull/${CHANGE_ID}/merge git checkout -qf FETCH_HEAD