Emilio Jesús Gallego Arias (Oct 15 2020 at 10:17): 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?
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.
Maxime Dénès (Oct 15 2020 at 10:41):Could we make it appear in the commit message meanwhile?
Maxime Dénès (Oct 15 2020 at 10:41):à la signed-off-by
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?
Emilio Jesús Gallego Arias (Oct 15 2020 at 10:47):I always get confused with the XXX-by tags
Emilio Jesús Gallego Arias (Oct 15 2020 at 10:47):Signed-off-by is more like for authros right?
Emilio Jesús Gallego Arias (Oct 15 2020 at 10:47):In Dune we use it to mark the commit agrees to the DCO
Maxime Dénès (Oct 15 2020 at 10:54):yeah I meant another similar tag
Emilio Jesús Gallego Arias (Oct 15 2020 at 11:04):That one could be OK indeed, I am not very familiar
Last updated: May 31 2023 at 17:01 UTC