Skip to content

Commit

Permalink
chore(.travis.yml): use git clean to clean out untracked files
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
rwbarton committed Jan 30, 2019
1 parent 54f4b29 commit a22aeec
Showing 1 changed file with 1 addition and 2 deletions.
3 changes: 1 addition & 2 deletions .travis.yml
Expand Up @@ -20,8 +20,7 @@ install:
- chmod +x $HOME/scripts/travis_long
- (git status | grep -e "Changes not staged for commit:"); RESULT=$?
- if [ $RESULT -eq 0 ]; then git checkout -f HEAD ; fi
- rm `git status | grep "\.lean" | sed "s/\.lean/.olean/"` || true
- rm `git status | grep "\.lean"` || true
- git clean -d -f -q
- rm mathlib.txt || true

jobs:
Expand Down

0 comments on commit a22aeec

Please sign in to comment.