Hey guys, was I constantly mistaken or does GitHub (bare-bones without bors) invoke workflows for PRs having merged the PR branch with destination branch (e.g. master). I have noticed this when issuing a PR with an old branch that no longer builds if it is merged with the current master.
I noticed the checkout actions uses some undocumented feature of GitHub, namely PR merge refs, it invokes:
git fetch --no-tags --prune --no-recurse-submodules --depth=1 origin +<some_long_hash>:refs/remotes/pull/42/merge
Yes, it does, which seems a good idea
Yes, I don't recall where it's documented exactly, but GitHub does say that PR workflow runs are done against a merged commit.
This isn't "enough" to replace bors, though, as the workflow is not rerun if the target branch is updated between the posting of the PR and the merging of the PR.