Retry for failed pushes (#150)

* Retry for failed pushes

* Nothing escape the Eye of Sauron

Author: sgugger

.github/workflows/build_main_documentation.yml

@@ -116,7 +116,9 @@ jobs:
           if [[ `git status --porcelain` ]]; then 
             git add .
             git commit -m "Updated with commit ${{ inputs.commit_sha }} See: https://github.com/huggingface/${{ inputs.package }}/commit/${{ inputs.commit_sha }}"
-            git push origin main
+            git push origin main ||
+            (echo "Failed on the first try, rebasing and pushing again" && git pull --rebase && git push origin main) ||
+            (echo "Failed on the second try, rebasing and pushing again" && git pull --rebase && git push origin main)
           else
             echo "No diff in the documentation."
           fi
@@ -134,7 +136,9 @@ jobs:
             if [[ `git status --porcelain` ]]; then
               git add ${{ inputs.notebook_folder }}
               git commit -m "Updated ${{ inputs.package }} doc notebooks with commit ${{ inputs.commit_sha }} \n\nSee: https://github.com/huggingface/${{ inputs.package }}/commit/${{ inputs.commit_sha }}"
-              git push origin master
+              git push origin master ||
+              (echo "Failed on the first try, rebasing and pushing again" && git pull --rebase && git push origin master) ||
+              (echo "Failed on the second try, rebasing and pushing again" && git pull --rebase && git push origin master)
             else
               echo "No diff in the notebooks."
             fi

.github/workflows/build_pr_documentation.yml

@@ -89,7 +89,9 @@ jobs:
           if [[ `git status --porcelain` ]]; then
             git add .
             git commit -m "Updated with commit ${{ inputs.commit_sha }} See: https://github.com/huggingface/${{ inputs.package }}/commit/${{ inputs.commit_sha }}"
-            git push origin main
+            git push origin main ||
+            (echo "Failed on the first try, rebasing and pushing again" && git pull --rebase && git push origin main) ||
+            (echo "Failed on the second try, rebasing and pushing again" && git pull --rebase && git push origin main)
           else
             echo "No diff in the documentation."
           fi

.github/workflows/delete_doc_comment.yml

@@ -40,7 +40,9 @@ jobs:
           if [[ `git status --porcelain` ]]; then
             git add .
             git commit -m "Closed PR ${{ inputs.pr_number }} in ${{ inputs.package }}"
-            git push origin main
+            git push origin main ||
+            (echo "Failed on the first try, rebasing and pushing again" && git pull --rebase && git push origin main) ||
+            (echo "Failed on the second try, rebasing and pushing again" && git pull --rebase && git push origin main)
           else
             echo "Branch was already deleted, nothing to do."
           fi