From e01e9e83cf6c5521cfa066b344a87f399541debb Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 29 Jul 2024 15:04:35 +0200 Subject: [PATCH] fix --- src/leanmonaco.ts | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/leanmonaco.ts b/src/leanmonaco.ts index ee6ba17..c0ccbb0 100644 --- a/src/leanmonaco.ts +++ b/src/leanmonaco.ts @@ -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)