Mirocom/EDK2-fork
1
0
Fork 0
Code Issues Pull Requests Actions 2 Packages Projects Releases Wiki Activity

.github: Compare collaborator GitHub ID's in single case

Browse Source 
Since case of a GitHub user name may by specified differently in the
`Maintainers.txt` file versus what is actually returned by the GitHub
API (actual case), convert both to lowercase for comparison.

Other GitHub user name inputs are directly from APIs and maintain
consistent casing.

Signed-off-by: Michael Kubacki <michael.kubacki@microsoft.com>
This commit is contained in:
Michael Kubacki
2025-05-12 15:08:20 -04:00
committed by mergify[bot]
parent 399a40e5cb
commit 607c58ef01
1 changed files with 2 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
.github/scripts/GitHub.py vendored
View File

@@ -228,8 +228,8 @@ def add_reviewers_to_pr(
)
# A user can only be added if they are a collaborator of the repository.
repo_collaborators = [c.login.strip() for c in repo_gh.get_collaborators() if c]
non_collaborators = [u for u in user_names if u not in repo_collaborators]
repo_collaborators = [c.login.strip().lower() for c in repo_gh.get_collaborators() if c]
non_collaborators = [u for u in user_names if u.lower() not in repo_collaborators]
excluded_pr_reviewers = [pr_author] + current_pr_reviewers + non_collaborators
new_pr_reviewers = [u for u in user_names if u not in excluded_pr_reviewers]