deploy: retry when git push fails

This commit is contained in:
linsui 2024-05-05 17:20:41 +08:00 committed by Michael Pöhn
parent 79586fd9e3
commit f82d648cb1

View file

@ -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)
origin.push(GIT_BRANCH) for _i in range(3):
try:
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():