Visual Code, restart and recheck all .lean files in project

Stream: lean4

[Paige Thomas]

Is there a command in Visual Code to reload and recheck all of the Lean code files in a project? Currently if I make a change in a file that is a dependency I go through and open each file and click restart file on each one that says it requires it, and wait for the orange bar to clear on all of them.
I currently don't have a file that imports all of the other Lean files, because there are name clashes, and I'm in the process of fixing that.

[Marc Huisinga]

The 'Project: Build Project' command in VS Code builds the full project and restarts the entire language server.

[Sebastian Ullrich]

You can make Lake build all your files without importing them all into one place, see e.g. https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/build.20all.20my.20code/near/418461467

[Paige Thomas]

Thank you!