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.
This commit is contained in:
bbhtt
2024-06-16 20:33:25 +05:30
parent 66fdbc8c56
commit 356942a3c5
+6 -2
View File
@@ -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}",