Rename "Install Elan" button

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:
     ```

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.
 

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}`