For `pull_request` events, `GITHUB_SHA` is not the SHA of the HEAD
commit of the pull request branch but of the merge commit created by
GitHub [1].  Apparently, this is even the case when there is no merge
commit because the action checks out the HEAD commit (bug?).

[1]: https://docs.github.com/en/free-pro-team@latest/actions/reference/events-that-trigger-workflows#pull_request