use `git clean` in ci-build script (see GPR#1067)

master
Damien Doligez 2017-03-27 15:54:56 +02:00
parent 21f9471434
commit f9c6cef483
1 changed files with 4 additions and 0 deletions

View File

@ -158,6 +158,10 @@ export LC_ALL=C
$make -f $makefile distclean || :
# `make distclean` does not clean the files from previous versions that
# are not produced by the current version, so use `git clean` in addition.
git clean -f -d -x
if $docheckout; then
git fetch origin
git reset --hard FETCH_HEAD