fix: less restrictive version parsing, closes #6

leanprover · Jan 27, 2021 · cc8bfda · cc8bfda
1 parent 24da3a0
commit cc8bfda
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/extension.ts b/src/extension.ts
@@ -33,7 +33,7 @@ async function checkLean4(): Promise<boolean> {
         // looks for a global (default) installation of Lean. This way, we can support
         // single file editing.
         const { stdout, stderr } = await promisify(exec)(cmd, {cwd: folderPath})
-        const filterVersion = /Lean \(version (\d+)\.(\d+)\.([^,]+), commit [^,]+, \w+\)/
+        const filterVersion = /version (\d+)\.\d+\..+/
         const match = filterVersion.exec(stdout)
         if (!match) {
             void window.showErrorMessage(`lean4: '${cmd}' returned incorrect version string '${stdout}'.`)