getting lean terminal commands on path (macos)

Stream: new members

[Homer White]

Hello, new member here, working with MacOS. I installed Lean through VSCode as per the manual, and I can use it fine within VSCode. However I now find that I need to run a lake update, but the lake command (and presumably other lean temrinal comands) are not on my path. The manual said to follow directions given at the end of installation to be able to access commands through the terminal, but I did not see any such directions during the installation process. Deos anyone know where the lean commands are stored on MacOS, or point me to the missing instructions? Thanks in advance.

[Matthew Ballard]

I am guessing ~/.elan/bin/ but you probably just need to source a bash/zsh file.

[Homer White]

Matthew Ballard said:

I am guessing ~/.elan/bin/ but you probably just need to source a bash/zsh file.

Thanks, @Matthew Ballard , that was it!