diff --git a/Jenkinsfile b/Jenkinsfile index b3ed0808..4ca27b77 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -97,7 +97,7 @@ try { git commit --author='Flatiron Jenkins ' --allow-empty -m 'Generated documentation for ${subdir}' -m '${env.BUILD_TAG} ${commit}' """ // note: credentials used above don't work (need JENKINS-28335) - sh "git push origin master" + sh "git push origin master || { git pull --rebase origin master && git push origin master ; }" } dir("$workDir/docker") { try { git(url: "ssh://git@github.com/TRIQS/docker.git", branch: env.BRANCH_NAME, credentialsId: "ssh", changelog: false) @@ -106,7 +106,7 @@ try { git commit --author='Flatiron Jenkins ' --allow-empty -m 'Autoupdate ${projectName}' -m '${env.BUILD_TAG}' """ // note: credentials used above don't work (need JENKINS-28335) - sh "git push origin ${env.BRANCH_NAME}" + sh "git push origin ${env.BRANCH_NAME} || { git pull --rebase origin ${env.BRANCH_NAME} && git push origin ${env.BRANCH_NAME} ; }" } catch (err) { echo "Failed to update docker repo" } }