From 356942a3c5f01ef5cdb483b94fa70c196d683036 Mon Sep 17 00:00:00 2001 From: bbhtt Date: Sun, 16 Jun 2024 18:47:51 +0530 Subject: [PATCH] merge: Don't error on incorrect usernames Github webui allows teams to be at-ed too, but add_to_collaborators accepts Github usersnames only https://pygithub.readthedocs.io/en/latest/github_objects/Repository.html?highlight=add_to_collaborators#github.Repository.Repository.add_to_collaborators So we should not error on wrong usernames being @-ed. --- .github/actions/merge/entrypoint.py | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/.github/actions/merge/entrypoint.py b/.github/actions/merge/entrypoint.py index 11d416d..71de188 100755 --- a/.github/actions/merge/entrypoint.py +++ b/.github/actions/merge/entrypoint.py @@ -225,8 +225,12 @@ def main(): collaborators = {user.replace("@", "") for user in command.split()[1:]} for user in collaborators: - print(f"adding {user} to collaborators") - repo.add_to_collaborators(user, permission="push") + try: + print(f"adding {user} to collaborators") + repo.add_to_collaborators(user, permission="push") + except github.GithubException: + print(f"Adding {user} failed") + pass close_comment = ( f"A repository for this submission has been created: {repo.html_url}",