diff options
author | Arnstein Ressem <aressem@oath.com> | 2018-08-28 15:28:29 +0200 |
---|---|---|
committer | Arnstein Ressem <aressem@oath.com> | 2018-08-28 15:28:29 +0200 |
commit | a906940d0b831e93ddf4c597001019e7137d457b (patch) | |
tree | b79dfe312fd0d2d9c04f093a49befbbcf043c993 /dist | |
parent | 7a10cb6bb7c8ac100226adfc0448f522387da27a (diff) |
Add simple retry for push on master.
Diffstat (limited to 'dist')
-rwxr-xr-x | dist/release-vespa-rpm.sh | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/dist/release-vespa-rpm.sh b/dist/release-vespa-rpm.sh index d2384c21b4e..dbd5565729c 100755 --- a/dist/release-vespa-rpm.sh +++ b/dist/release-vespa-rpm.sh @@ -22,7 +22,12 @@ git pull --rebase # Update the VERSION file on master to be the next releasable version echo "$VERSION" | awk -F. '{print $1"."($2+1)".0"}' > VERSION git commit -am "Updating VERSION file to next releasable minor version." -git push +for i in 1 2 3; do + if git push; then + break; + fi + git pull --rebase +done # Delete existing branch if exists and create new one git push --delete origin $RPM_BRANCH &> /dev/null || true |