mathlib3
f2cb5462 - fix(ci): setup git before nolints, rename secret (#2737)

Commit

5 years ago

fix(ci): setup git before nolints, rename secret (#2737) Oops, I broke the update nolints step on master. This should fix it.

Author

bryangingechen

Parents