diff options
| author | Théo Zimmermann | 2019-12-24 19:55:32 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-12-24 20:07:49 +0100 |
| commit | 8fd24bc02e5ed03593ee665d9a52903f97b8eac5 (patch) | |
| tree | 61a66efcb99dbcfb67962639344e7e5ce2be2e81 /kernel/type_errors.ml | |
| parent | c32e1c54c87231b6411d3002766972e18438fc4a (diff) | |
Update merging doc following the full move to teams.
Integrate merging doc in the main contributing document.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions