gistfile1.txt

At the time the PR was filed or updated:

         A---B    PR
        /
   C---D---E      main

GitHub create a merge commit to test the PR:

         A---B    PR
        /     \
   C---D---E---M  merged

At the time the workflow_run workflow runs:

         A---B    PR
        /
   C---D---E---F  main
   

                                        pull_request    pull_request_target     workflow_run

sha                                     M               E                       F
event.pull_request.head.sha             B               B                       -
event.pull_request.base.sha             E               E                       -
event.workflow_run.head_commit.id       -               -                       B
event.workflow_run.head_sha             -               -                       B

In order to detect changes in the PR, we need to compare M to E (which we can
only do from pull_request workflow) or compute D and inspect D..B.

If we are looking for changes to .github, the later option is equivalent to:

  git log --format=%H -n 1 .github   # find most recent commit to change .github

followed by checking if that commit is already in the base branch or not.

Turns out something like git log --exit-code HEAD --not BASE -- .github gets the job done.