diff options
| author | Hugo Herbelin | 2017-07-04 18:51:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-10-24 11:14:13 +0200 |
| commit | 341dcf85e43bd2569910426cfbcdc28032dfdb68 (patch) | |
| tree | cea15d9b1b91443b371b866dc2d47e064a8e9920 /kernel/type_errors.mli | |
| parent | 0897d0f642c19419c513f9609782436bebf28f5b (diff) | |
A missing newline after a comment.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions