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 13 2024 at 01:02 UTC