chore: group beta PR logs (#24236)

This commit is contained in:
Luke Parker 2026-04-25 10:42:33 +10:00 committed by GitHub
parent ec201623fb
commit cdc7d5f2ea
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -57,6 +57,19 @@ function lines(prs: PR[]) {
return prs.map((x) => `- #${x.number}: ${x.title}`).join("\n") || "(none)"
}
function group(title: string) {
if (process.env.GITHUB_ACTIONS !== "true") {
console.log(title)
return { [Symbol.dispose]() {} }
}
console.log(`::group::${title}`)
return {
[Symbol.dispose]() {
console.log("::endgroup::")
},
}
}
async function typecheck() {
console.log(" Running typecheck...")
@ -227,8 +240,8 @@ async function main() {
const failed: FailedPR[] = []
for (const [idx, pr] of prs.entries()) {
console.log(`\nProcessing PR ${idx + 1}/${prs.length} #${pr.number}: ${pr.title}`)
console.log()
using _ = group(`Processing PR ${idx + 1}/${prs.length} #${pr.number}: ${pr.title}`)
console.log(" Fetching PR head...")
try {
await $`git fetch origin pull/${pr.number}/head:pr/${pr.number}`