Stream: Coq devs & plugin devs

Topic: Multiple PRs involving the same head commit mess with checks

view this post on Zulip Jason Gross (May 20 2021 at 21:28):

I copied https://github.com/coq/coq/pull/13969/ to https://github.com/coq/coq/pull/14328 (same head commit, different branches, different repos), and now the checks on https://github.com/coq/coq/pull/13969 display as in progress. Is this a bug?

view this post on Zulip Gaëtan Gilbert (May 20 2021 at 22:04):

it's technically accurate and probably not worth worrying about

view this post on Zulip Théo Zimmermann (May 21 2021 at 10:06):

This is not a bug: GitHub doesn't associate checks to PRs but to commits. So there is nothing we can do about this.

Last updated: May 28 2023 at 13:30 UTC