diff --git a/scripts/checkout.sh b/scripts/checkout.sh index d629628b..0c6afe96 100755 --- 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 diff --git a/thylint/README.md b/thylint/README.md index 27652be2..8a51463f 100644 --- a/thylint/README.md +++ b/thylint/README.md @@ -20,6 +20,7 @@ that can be displayed as source annotation with the [yuzutech/annotations][1] ac - `disable`: a comma-separated list of warning classes to disable (default: none). One of `diag`, `find-proofs`, `sorry`, `axiom`, `style`. Do not use spaces between comma and warning class. +- `pr_num`: pull request number to check out, e.g. for `pull_request_target` triggers. - `token`: GitHub PA token to authenticate for private repos (optional) ## Example diff --git a/thylint/action.yml b/thylint/action.yml index f1abb4f4..b86eee27 100644 --- a/thylint/action.yml +++ b/thylint/action.yml @@ -10,6 +10,9 @@ inputs: token: description: 'GitHub token for read access to repository' required: false + pr_num: + description: 'Explicit pull request number to check out, e.g. for pull_request_target' + required: false disable: description: 'Comma-separated list (no spaces) of warning classes to disable (default: none)' required: false