diff options
| author | Emilio Jesus Gallego Arias | 2017-02-04 21:18:54 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-02-06 19:36:27 +0100 |
| commit | 348160a1c59da5c448a56a2e2802865f94a40ddc (patch) | |
| tree | 6a66f1710515de8ae9bbe8ea6f6c7aa310c42712 /kernel/type_errors.ml | |
| parent | e61e83758e129d455d664b65a1fe15ecac793186 (diff) | |
[travis] Run tests using a parallel matrix.
We also optimize `travis_wait` use.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions