diff options
| author | Gaëtan Gilbert | 2018-12-12 14:10:52 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-12-17 16:42:36 +0100 |
| commit | bb1c89a486d47dbf497756b8374337a6857a96de (patch) | |
| tree | 82e30800cd9c23a903b5cd6d528d1b8243e4a98f /kernel/type_errors.ml | |
| parent | 9349e0367d2d50b11ccd31c8f6d1979ebd52e555 (diff) | |
Set up CI with Azure Pipelines
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions