File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -57,6 +57,19 @@ function lines(prs: PR[]) {
5757 return prs . map ( ( x ) => `- #${ x . number } : ${ x . title } ` ) . join ( "\n" ) || "(none)"
5858}
5959
60+ function group ( title : string ) {
61+ if ( process . env . GITHUB_ACTIONS !== "true" ) {
62+ console . log ( title )
63+ return { [ Symbol . dispose ] ( ) { } }
64+ }
65+ console . log ( `::group::${ title } ` )
66+ return {
67+ [ Symbol . dispose ] ( ) {
68+ console . log ( "::endgroup::" )
69+ } ,
70+ }
71+ }
72+
6073async function typecheck ( ) {
6174 console . log ( " Running typecheck..." )
6275
@@ -227,8 +240,8 @@ async function main() {
227240 const failed : FailedPR [ ] = [ ]
228241
229242 for ( const [ idx , pr ] of prs . entries ( ) ) {
230- console . log ( `\nProcessing PR ${ idx + 1 } / ${ prs . length } # ${ pr . number } : ${ pr . title } ` )
231-
243+ console . log ( )
244+ using _ = group ( `Processing PR ${ idx + 1 } / ${ prs . length } # ${ pr . number } : ${ pr . title } ` )
232245 console . log ( " Fetching PR head..." )
233246 try {
234247 await $ `git fetch origin pull/${ pr . number } /head:pr/${ pr . number } `
You can’t perform that action at this time.
0 commit comments