Can't select Bash as Default Shell

Stream: new members

[n Simplex Pachinko]

Hello,
I'm attempting to install VS Code correctly. I have made it down the installation instructions (https://leanprover-community.github.io/install/windows.html) to as far as "install leanprover extension" to VS Code, and I am now attempting to select Bash as the default shell.
I hit Ctrl-Shift-p, which brought up the palette, I typed "select default", which showed "Terminal: Select Default Shell" as the only available option. When I clicked it, it states that the only two available shells are Command Prompt and Windows PowerShell.

My Bash is installed into a non-default location. Is that an issue?
I turned the External: Windows Exec path to the path of git-bash.exe . I then entered a test file and typed #lean 1+1 and it threw an error: "command expected Lean [1, 1]"
Anyone know where I'm going wrong?

[Kevin Buzzard]

#lean 1+1 isn't a command. How about #check 1+1?

[n Simplex Pachinko]

Hmm. True. I thought that the first time, I actually put in "#eval 1+1" per the help file, but just mistyped, but it's working now, either way.

[Kevin Buzzard]

PS I am not at all sure that changing the default shell is an essential part of the installation process; I would be tempted to just not worry. #check 1+1 will tell you that it's a natural number, #eval 1+1 will tell you which one it is.

[n Simplex Pachinko]

Now it has an "Info" problem: "2 Lean [1, 1]" . The 2 (line number?) is white, the rest is gray. This probably doesn't matter, since I'm getting the right answer. Thank you! Off to do the Natural Number Game.

[Mario Carneiro]

That's what it's supposed to look like

[Mario Carneiro]

The 2 is the result, the Lean is some extra info that vscode displays about the source of the hover text