add source folder

Stream: general

[Mark Ettinger]

How do I add a new source folder in the main project directory? I created a folder with new .lean files but I'm getting the error "unknown module prefix" when I try to "import NewDirectory.NewMyFile".

[Yury G. Kudryashov]

You need to add it as a library to lakefile.toml or lakefile.lean.