Avoid repeatedly downloading the same file

lean-dojo / LeanDojo

Tool for data extraction and interacting with Lean programmatically.

https://leandojo.org

MIT License

532 stars 77 forks source link

Avoid repeatedly downloading the same file #104

Closed darabos closed 8 months ago

darabos commented 8 months ago

I was hitting GitHub rate limits and it seemed to be caused by calling get_config("lean-toolchain") all the time, and downloading the config file over and over. This change fixed the issue for me.

yangky11 commented 8 months ago

Thanks!