From 203783ceba9de09f8770dc3665540a42387160c9 Mon Sep 17 00:00:00 2001
From: Dylan Simon <dylan@dylex.net>
Date: Tue, 4 Dec 2018 13:50:12 -0500
Subject: [PATCH] [jenkins] try a more robust git push

---
 Jenkinsfile | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Jenkinsfile b/Jenkinsfile
index b3ed0808..4ca27b77 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -97,7 +97,7 @@ try {
           git commit --author='Flatiron Jenkins <jenkins@flatironinstitute.org>' --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 <jenkins@flatironinstitute.org>' --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"
       } }