It seems that before, if `$src` isn’t a file, but a directory, that it would contain `Bar.lean` directly, and not `Foo/Bar.lean`. This seemd odd and would not allow dependencies to be included easily. |
||
|---|---|---|
| .. | ||
| bareStdenv | ||
| templates/pkg | ||
| bootstrap.nix | ||
| buildLeanPackage.nix | ||
| lake-dev.in | ||
| lean-dev.in | ||
| packages.nix | ||