-
Notifications
You must be signed in to change notification settings - Fork 83
Open
Description
When Elan is outdated, I see the following warning message when open vscode
Lean's version manager Elan is outdated: the installed version is 3.1.1, but a version of 4.0.0 is recommended.
Do you wish to update Elan?
[Proceed] [Update Elan]
vscode-lean4/vscode-lean4/src/utils/leanInstaller.ts
Lines 313 to 330 in d0f130d
| private updateElanPrompt(mode: UpdateElanMode): { message: string; item: 'Update Elan' } { | |
| switch (mode.kind) { | |
| case 'Manual': | |
| return { | |
| message: | |
| "This command will update Lean's version manager Elan to its most recent version.\n\n" + | |
| 'Do you wish to proceed?', | |
| item: 'Update Elan', | |
| } | |
| case 'Outdated': | |
| return { | |
| message: | |
| `Lean's version manager Elan is outdated: the installed version is ${mode.versions.currentVersion.toString()}, but a version of ${mode.versions.recommendedVersion.toString()} is recommended.\n\n` + | |
| 'Do you wish to update Elan?', | |
| item: 'Update Elan', | |
| } | |
| } | |
| } |
The problem is that the button labels are confusing: [Proceed] should have been named, say, [Proceed with current version] or [Do not] etc.
Metadata
Metadata
Assignees
Labels
No labels