thylint: accept PR number inputs

GitHub turns this into INPUT_PR_NUM, which is consumed by `scripts/checkout.sh`. Signed-off-by: Gerwin Klein <[email protected]>
seL4 · Jul 9, 2024 · c705c08 · c705c08
1 parent d8faf1b
commit c705c08
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 0 deletions.
diff --git 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
@@ -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