mirror of
https://github.com/f-droid/fdroidserver.git
synced 2025-09-13 22:42:29 +03:00
Merge branch 'deploy' into 'master'
deploy: retry when git push fails See merge request fdroid/fdroidserver!1480
This commit is contained in:
commit
08c553e1cb
1 changed files with 9 additions and 1 deletions
|
@ -837,7 +837,15 @@ def push_binary_transparency(git_repo_path, git_remote):
|
||||||
origin.set_url(git_remote)
|
origin.set_url(git_remote)
|
||||||
else:
|
else:
|
||||||
origin = gitrepo.create_remote('origin', git_remote)
|
origin = gitrepo.create_remote('origin', git_remote)
|
||||||
|
for _i in range(3):
|
||||||
|
try:
|
||||||
origin.push(GIT_BRANCH)
|
origin.push(GIT_BRANCH)
|
||||||
|
except git.GitCommandError as e:
|
||||||
|
logging.error(e)
|
||||||
|
continue
|
||||||
|
break
|
||||||
|
else:
|
||||||
|
raise FDroidException(_("Pushing to remote server failed!"))
|
||||||
|
|
||||||
|
|
||||||
def main():
|
def main():
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue