summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGabriel Scherer <gabriel.scherer@gmail.com>2017-10-07 13:26:21 +0200
committerGabriel Scherer <gabriel.scherer@gmail.com>2017-10-07 13:26:58 +0200
commitcc5bd1d199c54c4afb90faa5adfa8821998992ac (patch)
treeaa9844df4144d7dc1a9aa832b85baa5383b7425b
parent277b22eefc52a9dc9b1b0c896734db043dd9fc29 (diff)
downloadocaml-cc5bd1d199c54c4afb90faa5adfa8821998992ac.tar.gz
travis: test 'make clean'
(no change entry needed)
-rwxr-xr-x.travis-ci.sh2
1 files changed, 2 insertions, 0 deletions
diff --git a/.travis-ci.sh b/.travis-ci.sh
index a3977baefc..5c2cb8728e 100755
--- a/.travis-ci.sh
+++ b/.travis-ci.sh
@@ -79,6 +79,8 @@ EOF
# we would need to redo (small parts of) world.opt afterwards to
# use the compiler again
$MAKE check_all_arches
+ # check that the 'clean' target also works
+ $MAKE clean
}
CheckChangesModified () {