Skip to content

Support Repositories with Inner Lakefile #153

@andrewmw94

Description

@andrewmw94

Thanks for open sourcing this tool, it's great! I'd like to use it with projects such as https://github.com/cedar-policy/cedar-spec/tree/main/cedar-lean, which has a lake project in a subfolder instead of at the root. I forked LeanDojo and a work-in-progress PR here: #152.

To be more general, I think it would be great to support pointing this at any local lake project. I'm happy to contribute this if you agree it would be useful. My plan would be to

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions