Stream: Coq devs & plugin devs

Topic: Merge script


view this post on Zulip Pierre-Marie Pédrot (May 11 2020 at 10:21):

On #12129, the merge script wrote my review status as Ack-by, while I actually had accepted it. Is it a bug of the meta-data retrieval script. cc @Théo Zimmermann

view this post on Zulip Théo Zimmermann (May 11 2020 at 10:22):

I've seen this happens a number of times with my own reviews but I haven't looked into it yet.

view this post on Zulip Gaëtan Gilbert (May 11 2020 at 10:27):

If you fetch https://api.github.com/repos/coq/coq/pulls/12129/reviews there's only one ppedrot entry and it has state COMMENTED so more like a github bug

view this post on Zulip Théo Zimmermann (May 11 2020 at 10:28):

I was looking into this and saw the same thing. However, I don't think this is a GitHub bug. It's just that we have reached the pagination limit (30 reviews).

view this post on Zulip Théo Zimmermann (May 11 2020 at 10:29):

https://api.github.com/repos/coq/coq/pulls/12129/reviews?page=2 has the APPROVED review.

view this post on Zulip Théo Zimmermann (May 11 2020 at 10:29):

So I qualify this as a bug of the merge script.

view this post on Zulip Kenji Maillard (May 11 2020 at 10:34):

Btw, upon failure of the merging process (for instance if you don't have the credentials for pushing signing[edited]), the merge script can leave the repo on a partially failed merge . Not a big deal but might be a nice thing to clean up (not that I know how to do it)

view this post on Zulip Gaëtan Gilbert (May 11 2020 at 10:53):

WDYM? The merge script doesn't push so how do credentials matter?

view this post on Zulip Gaëtan Gilbert (May 11 2020 at 10:55):

So I qualify this as a bug of the merge script.

Indeed, opened https://github.com/coq/coq/issues/12300

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2020 at 12:54):

Maybe the automated cleaning process could be a bit dangerous knowing git , we can display some tip tho.


Last updated: Oct 16 2021 at 01:03 UTC