diff options
| author | Théo Zimmermann | 2017-11-10 12:41:21 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2017-11-13 21:16:56 +0100 |
| commit | 7e12c382483c4fcbc64456e141c314ff0c101527 (patch) | |
| tree | 009492b88b24eccf82bea8372a6cad44956d2425 /kernel/type_errors.ml | |
| parent | d9f79d97dbc503e149cba2df1b228a94d7ac970b (diff) | |
Remove useless file README.doc.
This file is useless because all the information it contains is also in INSTALL.doc.
The overall goal is to reduce the number of files at the root of the repository.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions