diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-07-20 13:14:38 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-07-20 13:14:38 +0200 |
| commit | 945d7bfa27b71137d86a4a46aeeced90d4b59303 (patch) | |
| tree | 438561788f99b0896eb905aeaf19b93e6687c3a5 /.travis.yml | |
| parent | 4d4ec6a095d01b6117ac3682d8a7882b1a2520e7 (diff) | |
| parent | d074e889b3cdfe8c292d3c52a4ed005789384fc0 (diff) | |
Merge branch 'v8.7'
Diffstat (limited to '.travis.yml')
| -rw-r--r-- | .travis.yml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/.travis.yml b/.travis.yml index 6de63d387..500fa990d 100644 --- a/.travis.yml +++ b/.travis.yml @@ -144,6 +144,7 @@ matrix: before_install: - brew update - brew install opam + - brew install gnu-time before_install: - if [ "${TRAVIS_PULL_REQUEST}" != "false" ]; then echo "Tested commit (followed by parent commits):"; git log -1; for commit in `git log -1 --format="%P"`; do echo; git log -1 $commit; done; fi |