Zulip Chat Archive

Stream: general

Topic: Co-authored-by

Joachim Breitner (Mar 16 2022 at 13:50):

Did bors get smarter about Co-Authored-by headers? I added them manually as advised in the PR template, but now we have

commit 717b11ecf5807c48409375806e38ca13ee2a356e
Author: Joachim Breitner <mail@joachim-breitner.de>
Date:   Wed Mar 16 11:53:35 2022 +0000

    feat(group_theory/noncomm_pi_coprod): homomorphism from pi monoids or groups (#11744)

    Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

    Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

Yakov Pechersky (Mar 16 2022 at 13:52):

If you used the github UI to commit a suggestion that someone else provided, not editing it, then it already knows:

Yakov Pechersky (Mar 16 2022 at 13:53):

And if they make commits explicitly, also:

Joachim Breitner (Mar 16 2022 at 13:55):

Right, that’s the non-squashed commits on the PR, and if we’d use Github’s merge, I see how that would work. But bors creates a squashed commit from the branch, and takes the commit description from the PR title, so I am somewhat (positively) surprised to see it automatically added.

Joachim Breitner (Mar 16 2022 at 13:56):

Maybe the template in
should indicate that this is not needed when co-authors are known to git.
Or better, bors should deduplicate the list of co-authors.
Or we just don’t worry :-)

Gabriel Ebner (Mar 16 2022 at 16:23):

bors only appends the author names, it doesn't look at the PR body at all.

Gabriel Ebner (Mar 16 2022 at 16:24):

There's also a weird bug where bors mixes up the email address and name of the author.

Eric Rodriguez (Mar 16 2022 at 16:25):

for reference: image.png

Kyle Miller (Mar 16 2022 at 16:26):

I didn't realize @Eric Wieser was a collective pseudonym

Bryan Gin-ge Chen (Mar 16 2022 at 16:28):

I'm not sure if it's bors or github, but I believe that can happen when someone opens a PR from a branch where they didn't author the first commit.

Gabriel Ebner (Mar 16 2022 at 16:30):


# If a user doesn't have a public email address in their GH profile
# then get the email from the first commit to the PR

Eric Wieser (Mar 16 2022 at 23:11):


Last updated: Aug 03 2023 at 10:10 UTC