Function update_branch

ci/scripts/github/update_branch.py:138–150

(user: str, repo: str, sha: str, branch_name: str)

def update_branch(user: str, repo: str, sha: str, branch_name: str) -> None:
    git(["fetch", "origin", sha])
    git(["reset", "--hard", "FETCH_HEAD"])
    try:
        git(["branch", "-D", branch_name])
    except RuntimeError:
        # Ignore failures (i.e. the branch did not exist in the first place)
        pass
    git(["checkout", "-b", branch_name])

    # Create and push the branch
    git(["push", "origin", "--force", branch_name])
    print(f"Pushed branch {branch_name} with commit {sha}")


if __name__ == "__main__":