checkout: allow an option PR number to be passed

If an PR explicit PR number is passed, check out that PR, otherwise check out GITHUB_REF. This enables pull_request_target actions to provide an explicit target. Signed-off-by: Gerwin Klein <[email protected]>
seL4 · Jul 9, 2024 · d8faf1b · d8faf1b
1 parent d2bd03d
commit d8faf1b
Showing 1 changed file with 10 additions and 2 deletions.
diff --git a/scripts/checkout.sh b/scripts/checkout.sh
@@ -17,8 +17,16 @@ else
   REPO_URL="https://${REPO_PATH}"
 fi
 
-echo "Cloning ${REPO_PATH}@${GITHUB_REF}"
+# if an explicit PR number is set as INPUT (e.g. for pull_request_target), prefer that
+if [ -n "${INPUT_PR_NUM}" ]
+then
+  REF="refs/pull/${INPUT_PR_NUM}/head"
+else
+  REF="${GITHUB_REF}"
+fi
+
+echo "Cloning ${REPO_PATH}@${REF}"
 git init -q .
 git remote add origin ${REPO_URL}
-git fetch -q --no-tags --depth ${DEPTH} origin +${GITHUB_REF}:refs/heads/test-revision
+git fetch -q --no-tags --depth ${DEPTH} origin +${REF}:refs/heads/test-revision
 git checkout -q test-revision