lake command not found from VS code terminal immediately ...

Stream: general

[Chemy]

Hello! :)
I want to use lean to participate in a seminar on it, but I reached a problem following the tutorial.

I follow the instructions:
Done with ELAN: https://leanprover-community.github.io/install/windows.html
Now I am here: https://leanprover-community.github.io/install/project.html

I am in the section Working on an existing project
I am at the step when I am asked to run lake exe cache get, but after I do it in my visual studio code terminal, then I get:

lake : The term 'lake' is not recognized as the name of a cmdlet, function, script file, or operable program. Check the spelling of the name, or if a path was includ
ed, verify that the path is correct and try again.
At line:1 char:1
+ lake exe cache get
+ ~~~~
    + CategoryInfo          : ObjectNotFound: (lake:String) [], CommandNotFoundException
    + FullyQualifiedErrorId : CommandNotFoundException

So, now I am not sure if mathlib4 is installed or not (the tutorial so far never mentioned it).
So, should I continue anyway? Or should I do something else?

SOLVED: I do not know why, but: I exited the VS Code, I entered it again, and it helped.

[Notification Bot]

A message was moved here from #general > lake exe cache get problems? by Ruben Van de Velde.