Skip to content

Commit 17c468c

Browse files
authored
fix: build project after "Download Project" (#791)
1 parent d08e333 commit 17c468c

1 file changed

Lines changed: 9 additions & 0 deletions

File tree

vscode-lean4/src/projectinit.ts

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -435,6 +435,15 @@ Open this project instead?`
435435
return
436436
}
437437

438+
const buildResult = await lakeRunner.build()
439+
if (buildResult.kind === 'Cancelled') {
440+
return
441+
}
442+
if (buildResult.kind === 'Error') {
443+
displayLakeRunnerError(buildResult, 'Cannot build downloaded project.')
444+
return
445+
}
446+
438447
await ProjectInitializationProvider.openNewFolder(projectFolder)
439448
})
440449

0 commit comments

Comments
 (0)