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?
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.
Could we make it appear in the commit message meanwhile?
à la signed-off-by
Yep, for sure. That would be easy to do. What "XXX-by" format should we use?
I always get confused with the XXX-by tags
Signed-off-by is more like for authros right?
In Dune we use it to mark the commit agrees to the DCO
yeah I meant another similar tag
That one could be OK indeed, I am not very familiar
Last updated: Oct 16 2021 at 09:07 UTC