mirror of
https://github.com/c-cube/sidekick.git
synced 2026-01-28 12:24:50 -05:00
[travis] Ubuntu doesn't have 'time' by default...
This commit is contained in:
parent
e266134efc
commit
6757910225
1 changed files with 1 additions and 0 deletions
|
|
@ -11,6 +11,7 @@ addons:
|
||||||
- avsm
|
- avsm
|
||||||
packages:
|
packages:
|
||||||
- opam
|
- opam
|
||||||
|
- time
|
||||||
before_install:
|
before_install:
|
||||||
- export OPAMYES=1
|
- export OPAMYES=1
|
||||||
- export OPAMVERBOSE=1
|
- export OPAMVERBOSE=1
|
||||||
|
|
|
||||||
Loading…
Add table
Reference in a new issue