mathlib3
a5c51665
- fix(ci): do not fail when detecting ported files more than 40 commits old (#17914)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
fix(ci): do not fail when detecting ported files more than 40 commits old (#17914) The previous action worked by using `git diff`, but this fails on shallow checkouts. This version hits the github API.
Author
eric-wieser
Parents
ac5a7cec
Loading