Skip to content

Commit

Permalink
fix: still start language client when project folder is invalid
Browse files Browse the repository at this point in the history
  • Loading branch information
mhuisi committed Nov 3, 2023
1 parent 2f3f44e commit a5e1034
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions vscode-lean4/src/utils/clientProvider.ts
Original file line number Diff line number Diff line change
Expand Up @@ -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}`);
}
Expand Down

0 comments on commit a5e1034

Please sign in to comment.