LeanDojo icon indicating copy to clipboard operation
LeanDojo copied to clipboard
verified publisher icon lean-dojo

[WIP] Support cedar-lean

Open andrewmw94 opened this issue 1 year ago • 2 comments

Changes to support lake projects that aren't at the root of a github repo. Applicable to projects like https://github.com/cedar-policy/cedar-spec/tree/main/cedar-lean

This is WIP and not ready to merge (e.g., we'd need to revert baef645)

andrewmw94 avatar Apr 04 '24 15:04 andrewmw94

Sorry for my poor python code. Any suggestions to make it more idiomatic are appreciated.

andrewmw94 avatar Apr 04 '24 15:04 andrewmw94

Thanks! I'm converting it to a PR draft, but please let me know when it's ready.

yangky11 avatar Apr 11 '24 13:04 yangky11