From 675791022503201ba35019fbd0f4a200822a113c Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Sat, 23 Jul 2016 14:47:52 +0200 Subject: [PATCH] [travis] Ubuntu doesn't have 'time' by default... --- .travis.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.travis.yml b/.travis.yml index c1c30668..c707458b 100644 --- a/.travis.yml +++ b/.travis.yml @@ -11,6 +11,7 @@ addons: - avsm packages: - opam + - time before_install: - export OPAMYES=1 - export OPAMVERBOSE=1