Skip to content

Commit

Permalink
chore: adjust for actual release
Browse files Browse the repository at this point in the history
  • Loading branch information
mhuisi committed Sep 8, 2023
1 parent 03962ae commit 414f67c
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 3 deletions.
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ and you should see something like this in the `Lean: Editor` output panel:
```
info: downloading component 'lean'
info: installing component 'lean'
Lean (version 4.0.0, commit a7efe5b60e86, Release)
Lean (version 4.0.0, commit ec941735c80d, Release)
```

See [Complete Setup](#complete-setup) for more information
Expand Down
4 changes: 2 additions & 2 deletions vscode-lean4/src/leanclient.ts
Original file line number Diff line number Diff line change
Expand Up @@ -550,9 +550,9 @@ export class LeanClient implements Disposable {
if (nightly_match) {
return new Date(parseInt(nightly_match[1]), parseInt(nightly_match[2]) - 1, parseInt(nightly_match[3]));
}
const release_match = /^leanprover\/lean4:v(\d+)-(\d+)-(\d+)$/.exec(toolchainVersion);
const release_match = /^leanprover\/lean4:(\d+)-(\d+)-(\d+)$/.exec(toolchainVersion);
if (release_match) {
return new Date(2023, 8, 30);
return new Date(2023, 9, 8);
}
if (toolchainVersion === 'leanprover/lean4:stable') {
return new Date(2022, 2, 1);
Expand Down

0 comments on commit 414f67c

Please sign in to comment.