diff options
| author | Théo Zimmermann | 2018-01-02 15:59:01 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2018-02-21 17:25:11 +0100 |
| commit | 7face8b53832621b733f900a4a92395c5ba97d34 (patch) | |
| tree | 4b79e84dc8eb18ea2351057fc3cb28cbaeb61f7d /kernel/type_errors.mli | |
| parent | aec63ba9c8f6840d98ba731640a786138d836343 (diff) | |
Remove redundant COPYRIGHT file.
This information is already present in CREDITS.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions