Stream: t-compiler/wg-rls-2.0

Topic: Pull requests

std::Veetaha (Apr 24 2020 at 14:39, on Zulip):

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
Florian Diebold (Apr 24 2020 at 14:48, on Zulip):

Yes, it does, which seems a good idea

Christopher Durham (Apr 25 2020 at 18:50, on Zulip):

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.

Last update: Sep 22 2020 at 01:45UTC