mathlib
829b49bd - chore(.travis.yml): use git clean to clean out untracked files (#659)

Commit
6 years ago
chore(.travis.yml): use git clean to clean out untracked files (#659) * chore(.travis.yml): use git clean to clean out untracked files and delete more obsolete olean files PR #641 involved renaming a directory. The old directory was still present in the cache, and in this situation `git status` lists the directory as a whole as untracked, so the grep did not find any `.lean` files.
Author
Committer
Parents
Loading