opened folder is not a valid lean4 project

Stream: new members

[stark]

I followed the tutorial in https://leanprover-community.github.io/install/project.html. But when I open the .lean file in subfolder 'MyProject' , the lean4 extension warns that 'Opened folder is not a valid Lean 4 project. Please open a valid Lean 4 project containing a 'lean-toolchain' file for full functionality.'

[stark]

there is already lean-toolchain in my_project

[Yaël Dillies]

Are you sure you opened the folder containing lean-toolchain and not a parent folder?

[stark]

Yaël Dillies said:

Are you sure you opened the folder containing lean-toolchain and not a parent folder?

That's it. Thanks