Correct. The GitHub Action was doing

`git pull origin ${{ github.head_ref || github.ref }}`

In the pull_request_target action, $github.ref is the name of the branch, which in this case included a curl request for a shell script, a pipe character, and bash.