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

@@ -36,6 +36,8 @@ jobs:
           route: GET /repos/${{ github.repository }}/pulls
 
       - name: Checkout branch
+        env:
+          BRANCH: ${{ github.event.workflow_run.head_branch }}
         # yamllint disable rule:line-length
         run: |
           PR_DATA=$(mktemp)
@@ -48,7 +50,7 @@ jobs:
           if [ ! -z "$PR" ]; then
             git checkout -b PR-$PR
           else
-            git checkout ${{ github.event.workflow_run.head_branch }} --
+            git checkout "${BRANCH}" --
           fi
         # yamllint enable rule:line-length