diff options
| author | Théo Zimmermann | 2017-09-07 15:15:14 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2017-09-08 09:59:38 +0200 |
| commit | b4958163084177157b416aaea2bde9d26ec2332b (patch) | |
| tree | d49b4e52f0aaacfbc7a2509fe7c806bc529d0894 /kernel/type_errors.mli | |
| parent | 92007cd55fdaa53dfbe2bd49a8f0a5c445031b27 (diff) | |
Move README.ci and link to it from CONTRIBUTING.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions