diff options
| author | Maxime Dénès | 2016-11-10 12:27:20 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-11-10 12:37:02 +0100 |
| commit | 5a95de009158be1166b3998b99cafbccf4a0b2fa (patch) | |
| tree | 178ab8e591de02b544c2c22901e42d5d1582284d /kernel/type_errors.ml | |
| parent | 3e19c53bffa95c6c6f4fd5006d54668f36694dd2 (diff) | |
Move OSX script.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions