lean-dojo / LeanDojo

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

fix missing GitHub token #138

Closed doragera closed 7 months ago

doragera commented 7 months ago

We are working on our own fork and I accidentally sent the pull request here, sorry. After we have tested it out ourselves on the fork we may send a pull request to this repo. The minor modifications are supporting private lean repos for tracing and speeding up Dojo.__enter__ function by removing unnecessary copying during the execution.