diff options
| author | Hugo Herbelin | 2016-04-26 05:53:40 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-16 17:43:29 +0200 |
| commit | 09d6ce5340a818f24a85d568aab6502233e10273 (patch) | |
| tree | 9c5e976104b503017886a76c4f54c8fbcbed821d /kernel/type_errors.mli | |
| parent | 63ac502a4ea7f5c81346deeecfcf0d69d063a130 (diff) | |
Fixing space in an error message.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions