[Python-Dev] Re: Adding GitHub usernames to the developer log

I'm personally fine listing GItHub usernames in the devguide's developer list, but I'm also not trying to be anonymous on GitHub. But I will say that listing our GitHub usernames with our real names is not required to tell who is a core developer. In GitHub's UI there are multiple places it will tell you if a person is a member of the repository/team (e.g. hover cards, each comment a teammate makes).