diff options
| author | Enrico Tassi | 2019-01-09 14:01:51 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-01-10 16:39:50 +0100 |
| commit | 325f7ffb27496c8017d50712fe100658ea39bf2b (patch) | |
| tree | 5b48fb07bb193772d672aeccf4c55016c9e07356 /kernel/type_errors.ml | |
| parent | 468050a3831cedf63d7dbdb289d5824097bbe1e0 (diff) | |
[ci] compile with -quick & validate after vio2vo
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions