Zulip Chat Archive

Stream: new members

Topic: emails for co authored by


view this post on Zulip Yakov Pechersky (Sep 10 2020 at 16:44):

When submitting a PR or commits, where is a good place to find the emails of the coauthors to include?

view this post on Zulip Bryan Gin-ge Chen (Sep 10 2020 at 16:47):

If they've committed to mathlib before, you can try git log --author="<some part of their name or username>" in a local clone of mathlib.

view this post on Zulip Johan Commelin (Sep 10 2020 at 17:06):

It would be great if bors would accept github usernames... but I have no time to write that feature for them


Last updated: May 08 2021 at 10:12 UTC