github: prevent script injections via PR branch names

Prior this commit, ${{ github.event.workflow_run.head_branch }} got
expanded in the bash script. A malicious actor could inject
an arbitrary shell script. Since this action has access to a token
with write rights the malicious actor can easily steal this token.

This commit moves the expansion into an env block where such an
injection cannot happen. This is the preferred way according to the
github docs:
https://docs.github.com/en/actions/security-guides/security-hardening-for-github-actions#using-an-intermediate-environment-variable

.github/workflows/trigger-gitlab.yml

@@ -35,6 +35,8 @@ jobs:
           route: GET /repos/${{ github.repository }}/pulls
 
       - name: Checkout branch
+        env:
+          BRANCH: ${{ github.event.workflow_run.head_branch }}
         run: |
           PR_DATA=$(mktemp)
           # use uuid as a file terminator to avoid conflicts with data content
@@ -46,7 +48,7 @@ jobs:
           if [ ! -z "$PR" ]; then
             git checkout -b PR-$PR
           else
-            git checkout ${{ github.event.workflow_run.head_branch }}
+            git checkout "${BRANCH}"
           fi
 
       - name: Push to gitlab