Stream: Coq devs & plugin devs

Topic: coqbot merge metadata


view this post on Zulip Gaëtan Gilbert (Aug 05 2020 at 12:01):

Currently coqbot merge commits are like

Author:     coqbot <coqbot@users.noreply.github.com>
AuthorDate: Tue Aug 4 19:05:56 2020 +0200
Commit:     GitHub <noreply@github.com>
CommitDate: Tue Aug 4 19:05:56 2020 +0200

Having "Github" as the committer seems pretty strange
also shouldn't whoever gave coqbot the order be the author?

view this post on Zulip Théo Zimmermann (Aug 05 2020 at 13:58):

We're using GitHub's merge feature internally to have merge commits keep being signed (because we're not going to deploy a GPG key on our bot server), so I think the committer is likely going to stay GitHub (as is the case on any project using the merge button). Once we turn @coqbot into a proper GitHub App, we should be able to change the author's name. In the meantime, all we could do would be to add the merger as a co-author (in the merge commit).


Last updated: Oct 16 2021 at 03:02 UTC