diff options
| author | Enrico Tassi | 2020-11-24 16:47:25 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2020-11-26 11:20:13 +0100 |
| commit | 66370041661beb850c20d53d43111674a32d84b2 (patch) | |
| tree | 1d7cd1f2bb83a77fe382c6c4d72b11a373a40ed6 /kernel/type_errors.ml | |
| parent | e79430126e2d0ec55aec5937c53abba22f0df307 (diff) | |
[ci] add job for interval
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions