remove additional redundant "press any key to exit"

[lovettchris]

fix: remove additional redundant "press any key to exit" that was happening only on windows.
fix: remove reference to "Lean 3" in NoDefaultToolchain error message.

The reason for this "where installation happens in a console that may have opened just for this purpose" is no longer valid. The latest vscode extension when you install elan, you now get "press any key to continue" twice, which is odd, so this fixes that making the vscode extension experience consistent across platforms.

[Kha]

A bit late, but I hope this doesn't break/affect the Lean 3 extension's Lean installation? /cc @gebner

[lovettchris]

A bit late, but I hope this doesn't break/affect the Lean 3 extension's Lean installation? /cc @gebner

I just tested bootstrapping of lean3 from the vscode lean3 extension and it was able to download and install lean just fine, so looks like it still works.

[gebner]

I just tested bootstrapping of lean3 from the vscode lean3 extension and it was able to download and install lean just fine, so looks like it still works.

From what I can tell, the change isn't released yet, right?

Either way, the change looks innocent enough and I don't expect it to break anything. To be on the safe side we could post a heads-up on zulip once the release is out.

[lovettchris]

I just tested bootstrapping of lean3 from the vscode lean3 extension and it was able to download and install lean just fine, so looks like it still works.

From what I can tell, the change isn't released yet, right?

Either way, the change looks innocent enough and I don't expect it to break anything. To be on the safe side we could post a heads-up on zulip once the release is out.

I installed https://github.com/leanprover/vscode-lean changed it to run my locally build elan-init.sh and then invoke my locally built elan-init.exe and it worked fine, including the press enter key to continue prompt.

[Kha]

It's at https://github.com/leanprover/vscode-lean. But I made testing easier by going ahead and releasing the change :) .

[lovettchris]

It's at https://github.com/leanprover/vscode-lean. But I made testing easier by going ahead and releasing the change :) .

Thanks, I tested version 1.1.1 and found another redundant prompt... See #48