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
I've seen this happens a number of times with my own reviews but I haven't looked into it yet.
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
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).
https://api.github.com/repos/coq/coq/pulls/12129/reviews?page=2 has the APPROVED review.
So I qualify this as a bug of the merge script.
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)
WDYM? The merge script doesn't push so how do credentials matter?
So I qualify this as a bug of the merge script.
Indeed, opened https://github.com/coq/coq/issues/12300
Maybe the automated cleaning process could be a bit dangerous knowing git , we can display some tip tho.
Last updated: Jun 08 2023 at 04:01 UTC