fix: confusing elan installation prompt (#576)

leanprover · Jan 30, 2025 · c10f042 · c10f042
1 parent 256a36c
commit c10f042
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/vscode-lean4/src/utils/leanInstaller.ts b/vscode-lean4/src/utils/leanInstaller.ts
@@ -313,7 +313,7 @@ export class LeanInstaller {
 
         const prompt =
             'Elan installation successful!\n\n' +
-            'Do you want Elan in VS Code to continue downloading and installing Lean versions automatically, or would you prefer it to ask for confirmation before downloading and installing new Lean versions?\n' +
+            'Do you want Elan in VS Code to download and install Lean versions automatically, or would you prefer it to ask for confirmation before downloading and installing new Lean versions?\n' +
             'Asking for confirmation is especially desirable if you are ever using a limited internet data plan or your internet connection tends to be slow, whereas automatic installs are less tedious on fast and unlimited internet connections.'
 
         const choice = await displayNotificationWithInput(