Stream: Coq devs & plugin devs

Topic: coqbot merging does not include merger information


view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2020 at 10:17):

A useful bit of information we had in the past is who merged a particular PR, this seems to have been lost with the coqbot: merge now setup, right?

view this post on Zulip Théo Zimmermann (Oct 15 2020 at 10:32):

Right. This is something that could be fixed but would need more work: GitHub Apps can impersonate GitHub users, but this is not supported in the coqbot code yet.

view this post on Zulip Maxime Dénès (Oct 15 2020 at 10:41):

Could we make it appear in the commit message meanwhile?

view this post on Zulip Maxime Dénès (Oct 15 2020 at 10:41):

à la signed-off-by

view this post on Zulip Théo Zimmermann (Oct 15 2020 at 10:41):

Yep, for sure. That would be easy to do. What "XXX-by" format should we use?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2020 at 10:47):

I always get confused with the XXX-by tags

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2020 at 10:47):

Signed-off-by is more like for authros right?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2020 at 10:47):

In Dune we use it to mark the commit agrees to the DCO

view this post on Zulip Maxime Dénès (Oct 15 2020 at 10:54):

yeah I meant another similar tag

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2020 at 11:04):

That one could be OK indeed, I am not very familiar


Last updated: Oct 16 2021 at 09:07 UTC