leanproject build just one file

Stream: new members

[Joachim Breitner]

Can I invoke leanproject build in a way that it only builds the .olean files for one particular files’ dependencies?

[Adam Topaz]

lean --make foldername/filename.lean should do it.