mathlib
32052b86 - chore(ci): remove working directory on self-hosted (#11645)

Commit
3 years ago
chore(ci): remove working directory on self-hosted (#11645) Mathlib now takes several gigabytes to build. This addresses some of the space issues on the CI machines.
Author
Parents
Loading