search

lean-dojo / LeanDojo

Tool for data extraction and interacting with Lean programmatically.
https://leandojo.org
MIT License
536 stars 80 forks source link

Alternative function to LeanGitRepo #185

Closed LuoKaiGSW closed 1 month ago

LuoKaiGSW commented 1 month ago

I have a Lean4 project file, but I cannot upload it to Git because it contains company data. Is there any other function similar to LeanGitRepo that allows me to read and track the local git repository? Looking forward to your reply. Thank you!

yangky11 commented 1 month ago

Is https://github.com/lean-dojo/LeanDojo/pull/179 something you're looking for? I'll review the code and merge it when I get a chance.

LuoKaiGSW commented 1 month ago

Is #179 something you're looking for? I'll review the code and merge it when I get a chance.

Thank you,@yangky11 It works!