diff options
| author | Michael Soegtrop | 2018-04-05 16:15:04 +0200 |
|---|---|---|
| committer | Michael Soegtrop | 2018-04-05 16:15:04 +0200 |
| commit | 10e7b9b20319a8c17eb7e3fe8b4516c370470c97 (patch) | |
| tree | 124f6b96b9e4073fa36483d6ede9a511691416db /kernel/type_errors.ml | |
| parent | 116a790f1a20cce16ba906ee9bf34b4681f69377 (diff) | |
Fixes issue #7172 (don't include MinGW make in install)
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions