diff --git a/vscode-lean4/src/utils/clientProvider.ts b/vscode-lean4/src/utils/clientProvider.ts index cea8611b9..d6591a0a7 100644 --- a/vscode-lean4/src/utils/clientProvider.ts +++ b/vscode-lean4/src/utils/clientProvider.ts @@ -198,9 +198,9 @@ export class LeanClientProvider implements Disposable { return } - await this.checkIsValidProjectFolder(client.folderUri) - await client.openLean4Document(document) + + await this.checkIsValidProjectFolder(client.folderUri) } catch (e) { logger.log(`[ClientProvider] ### Error opening document: ${e}`); }