Closed fchapoton closed 2 years ago
hmm, not sure how my innocuous changes could have broken the CI
hmm, not sure how my innocuous changes could have broken the CI
Yes, it's definitely not you --- I believe it is this https://github.com/actions/checkout/issues/956.
I fixed the CI issue in master, so if you merge that in all checks should pass.
green lights, indeed
hopefuly done with enough care :owl: