Deal with diverging capitalization of usernames

OpenRailAssociation / github-org-manager

Manage a GitHub organization, its members, teams, repository permissions and more

Apache License 2.0

6 stars 2 forks source link

Deal with diverging capitalization of usernames #40

Closed mxmehl closed 3 months ago

mxmehl commented 3 months ago

Fix #38

If a GitHub username has a different capitalization from the configuration, this lead to strange behaviour in syncing team memberships and permissions.

This PR should fix this.