diff --git a/README.md b/README.md index 8c9cb5e75..d4c7dc22e 100644 --- a/README.md +++ b/README.md @@ -19,9 +19,9 @@ containing the following: 1. Open your file `hello.lean`. 1. If `Lean` is not yet installed on your system you will see a prompt like this: - ![prompt](vscode-lean4/media/install-elan.png) + ![prompt](vscode-lean4/media/install-lean.png) -1. Click the `Install Lean using Elan` option and enter any default options that appear in the terminal window. +1. Click the `Install Lean` option and enter any default options that appear in the terminal window. 1. After this succeeds the correct version of Lean will be installed by `elan` and you should see something like this in the `Lean: Editor` output panel: ``` diff --git a/docs/bootstrapping.md b/docs/bootstrapping.md index 8521aaad8..1c506dbbd 100644 --- a/docs/bootstrapping.md +++ b/docs/bootstrapping.md @@ -16,7 +16,7 @@ yet and in that case `getLeanVersion` calls `testLeanVersion` on the ![prompt](images/InstallPrompt.png) -If the user clicks `Install Lean using Elan` then this will happen +If the user clicks `Install Lean` then this will happen and elan will be installed in the default location and a stable build of Lean will also be installed. diff --git a/vscode-lean4/media/install-elan.png b/vscode-lean4/media/install-elan.png deleted file mode 100644 index 285b49108..000000000 Binary files a/vscode-lean4/media/install-elan.png and /dev/null differ diff --git a/vscode-lean4/media/install-lean.png b/vscode-lean4/media/install-lean.png new file mode 100644 index 000000000..14e9af708 Binary files /dev/null and b/vscode-lean4/media/install-lean.png differ diff --git a/vscode-lean4/src/utils/leanInstaller.ts b/vscode-lean4/src/utils/leanInstaller.ts index 446194472..2452efb5e 100644 --- a/vscode-lean4/src/utils/leanInstaller.ts +++ b/vscode-lean4/src/utils/leanInstaller.ts @@ -147,7 +147,7 @@ export class LeanInstaller { // note; we keep the LeanClient alive so that it can be restarted if the // user changes the Lean: Executable Path. - const installItem = 'Install Lean using Elan'; + const installItem = 'Install Lean'; let prompt = 'Failed to start \'lean\' language server' if (path){ prompt += ` from ${path}`