mathlib3
b3eabc16 - hack(ci): run lean make twice (#7192)

Commit
5 years ago
hack(ci): run lean make twice (#7192) At the moment running `lean --make src` after `leanproject up` will recompile some files. Merging this PR should have the effect of uploading these newly compiled olean files. This also makes github actions call `lean --make src` twice to prevent this problem from happening in the first place.
Author
Parents
Loading