Minor fix to remove CI node warning

lean-dojo / LeanDojo

Tool for data extraction and interacting with Lean programmatically.

https://leandojo.org

MIT License

536 stars 80 forks source link

Minor fix to remove CI node warning #178

Closed Peiyang-Song closed 2 months ago

Peiyang-Song commented 2 months ago

This removes the warning message from CI runs:

The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2.
For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/.

(tested)