diff options
| author | Théo Zimmermann | 2019-08-22 19:06:32 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-08-22 19:06:32 +0200 |
| commit | 0fc73b31859abb42f3fccf018497b33dfa49c33b (patch) | |
| tree | dbbcfc278a2965f6aaf8e73aa1c765395f7c5e44 /kernel/type_errors.ml | |
| parent | 45db028fa0ffbdd77cf87dc73f9d59d488e1c7b6 (diff) | |
[gitlab/ci] Do not wait for all builds to finish to run the tests.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions