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?
it's technically accurate and probably not worth worrying about
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: Oct 16 2021 at 09:07 UTC