[size-report] checkout pull request head (#11724)

This commit is contained in:
Yakun Xu
2025-07-15 10:48:46 -07:00
committed by GitHub
parent e72e68a05e
commit d4734df8bb
3 changed files with 15 additions and 2 deletions
+8
View File
@@ -54,6 +54,14 @@ get_pr_body()
{
local pr
if [[ -z ${PR_BODY+x} ]]; then
echo 'PR_BODY is not set' >&2
else
echo 'PR_BODY is set' >&2
echo "${PR_BODY}"
return 0
fi
[[ ${GITHUB_ACTIONS+x} && ${GITHUB_REF-} =~ ^refs/pull/[0-9]+/merge ]] || {
echo 'Not a pull request.' >&2
return 0