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.