Commit 2024-11-20 11:42 7d4e3bb7

View on Github →

chore(discover-lean-pr-testing): properly fetch tags (#19204) Instead of guessing the dates of the latest two tags in the lean4-nightly repo, we list the available remote tags and take the last two. We then fetch them with a shallow depth, to avoid cloning the entire repo. After that we parse the commit log between these two tags.

Estimated changes