Skip to content

Commit

Permalink
fix
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster committed Jul 29, 2024
1 parent 10fb032 commit e01e9e8
Showing 1 changed file with 1 addition and 2 deletions.
3 changes: 1 addition & 2 deletions src/leanmonaco.ts
Original file line number Diff line number Diff line change
Expand Up @@ -121,8 +121,7 @@ export class LeanMonaco {
{appendLine: () => {}
} as any,
setupMonacoClient(this.getWebSocketOptions(options)),
checkLean4ProjectPreconditions,
(docUri: ExtUri) => { return true }
checkLean4ProjectPreconditions
)

this.taskGutter = new LeanTaskGutter(this.clientProvider, {asAbsolutePath: (path: string) => Uri.parse(`${new URL('vscode-lean4/vscode-lean4/' + path, import.meta.url)}`),} as any)
Expand Down

0 comments on commit e01e9e8

Please sign in to comment.