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 to (same head commit, different branches, different repos), and now the checks on 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: Feb 22 2024 at 04:02 UTC