From f82d648cb147c42032549fb59bdeecfaa3c52ee4 Mon Sep 17 00:00:00 2001 From: linsui Date: Sun, 5 May 2024 17:20:41 +0800 Subject: [PATCH] deploy: retry when git push fails --- fdroidserver/deploy.py | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/fdroidserver/deploy.py b/fdroidserver/deploy.py index 6daa7068..1e28961d 100644 --- a/fdroidserver/deploy.py +++ b/fdroidserver/deploy.py @@ -837,7 +837,15 @@ def push_binary_transparency(git_repo_path, git_remote): origin.set_url(git_remote) else: 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():