diff --git a/docs/tools/release.sh b/docs/tools/release.sh index 389b63ace7f..035581534f1 100755 --- a/docs/tools/release.sh +++ b/docs/tools/release.sh @@ -31,9 +31,11 @@ then git add * git add ".nojekyll" - # Push to GitHub rewriting the existing contents. git commit --quiet -m "Add new release at $(date)" - git push --force origin master + + # Push to GitHub rewriting the existing contents. + # Sometimes it does not work with error message "! [remote rejected] master -> master (cannot lock ref 'refs/heads/master': is at 42a0f6b6b6c7be56a469441b4bf29685c1cebac3 but expected 520e9b02c0d4678a2a5f41d2f561e6532fb98cc1)" + for _ in {1..10}; do git push --force origin master && break; sleep 5; done if [[ ! -z "${CLOUDFLARE_TOKEN}" ]] then