Lean project as a subfolder of a larger project

Stream: lean4

[Eric Rodriguez]

.
└── MyProject
    └── src
        ├── Foo
        │   └── LeanStuff
        │       ├── LeanStuff
        │       │   ├── a file.lean
        │       │   └── etc
        │       ├── LeanStuff.lean
        │       ├── lakefile.lean
        │       └── lean-toolchain
        ├── FooBar
        └── Bar
            └── BarFoo

Is it possible to have a directory structure like this and still be able to run the inner LeanStuff project as a Lean project? If I open the root of this project with VSCode, I am not allowed to run the Lean project, it complains about a lean-toolchain, which makes sense, but if I open LeanStuff, then I also can't interact with the rest of my files.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

@Eric Rodriguez you can use 'Add folder to workspace' on LeanStuff/. VSCode can handle opening a subfolder of another open folder. And you can also give thumbs-up to vscode-lean4#138 :)

[Eric Rodriguez]

Thanks! This seems to work just fine thankfully :) Is 138 a hope to make this process a little more seamless?