Pierre-Marie Pédrot (May 11 2020 at 10:21): 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
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.
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
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).
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.
Théo Zimmermann (May 11 2020 at 10:29):So I qualify this as a bug of the merge script.
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)
Gaëtan Gilbert (May 11 2020 at 10:53):WDYM? The merge script doesn't push so how do credentials matter?
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
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: Nov 29 2023 at 18:01 UTC