Could not find "Select Default Shell"

Stream: new members

[AnduinHS]

My lean on VS Code somehow does not work (which means it used to work).(For example, after I entering #eval 1+1 , the green line does not appear underneath #eval 1+1, and hovering the mouse over it I could not see 2 displayed. And it says "'Lean.DisplayGoal' not found")(maybe because I have deleted the previous opening settings(JSON)). I tried to follow https://leanprover-community.github.io/install/windows.html again to make it work. All other things seemed great. However, When I type Select Default Shell, I could not find it. 1.PNG So I have tried Select Default Profile and adds Git Bash to it. However, it doesn't work.
Should I unist and re-install VS Code?

[Johan Commelin]

Do you use VScode for other things?

[Johan Commelin]

If not, re-installing it seems harmless, so I would try it.

[AnduinHS]

ok

[Alex J. Best]

I think VScode has changed the name of the select default shell option to select default profile (microsoft/vscode#118790), I've PRed the fix to the site at leanprover-community/leanprover-community.github.io#199

[AnduinHS]

Now I know my problem. My DNS(or sth else) was reset by Chinese "Great FireWall". It says "info: downloading installer
curl: (56) OpenSSL SSL_read: Connection was reset, errno 10054
elan: command failed: curl -sSf https://github.com/leanprover/elan/releases/latest
". I should find some other way or have another in some other time.