diff options
| author | Théo Zimmermann | 2020-01-20 11:00:52 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-01-20 11:04:17 +0100 |
| commit | ce8c8981e04a2955ae7ada9a00be84a16fc8dd67 (patch) | |
| tree | bddb302db5c3f0188881926a1a048b8b0a6104a8 /kernel/type_errors.ml | |
| parent | 26bf92e978eca1f405b302a2e02b1cadc4723b76 (diff) | |
Dispatch code ownership of files in dev/doc.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions