diff options
| author | Arnaud Spiwack | 2017-12-08 21:43:12 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2017-12-08 21:43:12 +0100 |
| commit | 319a3c230e9f9ec5a8a5bea9e07b6b8d17444ac9 (patch) | |
| tree | aa04a1ef7b7f4059034df5b11c3206d3855e0b99 /kernel/type_errors.mli | |
| parent | d606a85d53fbd0227b15e18701e2ac4c9d911f34 (diff) | |
Revert "CI: poc Circleci configuration"
Committed on master by mistake. Clearly I'm too clumsy to be trusted
with push rights.
This reverts commit d606a85d53fbd0227b15e18701e2ac4c9d911f34.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions