Stream: new members
Topic: emails for co authored by
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?
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.
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