The --deps flag failed when a .olean file existed next to its source .lean file. This fix makes Lean consider only .lean files when looking for dependences.
Pull Request Description
Ensure you have read the contribution guide before filling in a description of the
pull request, regardless of whether it is complete or a work in progress.
All Pull Requests should include test case(s) which demonstrates the intended
behavior of a feature, or a regression test demonstrating that the fix resolves
the issue.
The
--depsflag failed when a.oleanfile existed next to its source.leanfile. This fix makes Lean consider only.leanfiles when looking for dependences.Pull Request Description
Ensure you have read the contribution guide before filling in a description of the pull request, regardless of whether it is complete or a work in progress. All Pull Requests should include test case(s) which demonstrates the intended behavior of a feature, or a regression test demonstrating that the fix resolves the issue.