Fix missing occurrence of branch name

ogrisel · ogrisel · commit e92ae0102a08 · 2020-12-01T10:25:38.000+01:00
diff --git a/.github/workflows/sync_pull_request.yml b/.github/workflows/sync_pull_request.yml
@@ -22,13 +22,13 @@ jobs:
           # Assign the contributor-specified branch name to an environment
           # variable to sanitize it and avoid arbitrary bash code injection by
           # non-privileged users.
-          HEAD_REF: ${{ github.event.pull_request.head.ref }}
+          PR_HEAD_REF: ${{ github.event.pull_request.head.ref }}
         run: |
           set -xe
           git remote add pr_remote ${{ github.event.pull_request.head.repo.html_url }}
-          git fetch pr_remote $HEAD_REF
-          git checkout -b pr_branch pr_remote/$HEAD_REF
+          git fetch pr_remote $PR_HEAD_REF
+          git checkout -b pr_branch pr_remote/$PR_HEAD_REF
           git config user.name github-actions
           git config user.email github-actions@github.com
           git merge origin/master
-          git push pr_remote HEAD:${{ github.event.pull_request.head.ref }}
+          git push pr_remote HEAD:$PR_HEAD_REF
