search

lean-dojo / LeanDojo

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

Ignore rmtree Errors #173

Closed yangky11 closed 2 weeks ago

yangky11 commented 2 weeks ago

https://github.com/lean-dojo/LeanDojo/issues/168

yangky11 commented 2 weeks ago

I'll also re-build the docs and pypi wheels after merging into main

Peiyang-Song commented 2 weeks ago

LGTM, thank you! Merging into main.