Stream: Coq devs & plugin devs

Topic: merge-pr.sh?


view this post on Zulip Gaëtan Gilbert (Jun 07 2021 at 09:36):

Is it time to remove this script? We have @coqbot: merge now to replace it, and having 2 ways to merge is kinda strange

view this post on Zulip Pierre-Marie Pédrot (Jun 07 2021 at 09:37):

AFAIK the author of the merge is still not taken into account by coqbot

view this post on Zulip Pierre-Marie Pédrot (Jun 07 2021 at 09:38):

this should be fixed before removing the script

view this post on Zulip Michael Soegtrop (Jun 07 2021 at 09:38):

I would appreciate some documentation on what coqbot does in case of warnings or errors - e.g. what it enforces. For merge-pr.sh this is more obvious and one always can decide against the final push.

view this post on Zulip Gaëtan Gilbert (Jun 07 2021 at 09:39):

Pierre-Marie Pédrot said:

AFAIK the author of the merge is still not taken into account by coqbot

it is
see our latest merge commit https://github.com/coq/coq/commit/19b489a7f87928dcfe0687c7dd9bef4ed7aaebed

view this post on Zulip Pierre-Marie Pédrot (Jun 07 2021 at 09:40):

where is the relevant data?

view this post on Zulip Pierre-Marie Pédrot (Jun 07 2021 at 09:41):

I don't see anything with git log

view this post on Zulip Gaëtan Gilbert (Jun 07 2021 at 09:41):

the Co-authored-by in the commit message

view this post on Zulip Pierre-Marie Pédrot (Jun 07 2021 at 09:41):

ah, ok


Last updated: Oct 16 2021 at 02:03 UTC