diff options
| author | Maxime Dénès | 2016-11-15 18:11:34 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-11-15 18:11:34 +0100 |
| commit | 3a51aa7265f35dd3cbf3f7bff858d663e4406146 (patch) | |
| tree | ade3adfabf9e288a164769e0457fda6e49ac1b24 /kernel/type_errors.ml | |
| parent | dfefd12ee432e5b0d145934e74bb939ddecfa522 (diff) | |
| parent | 4b8f19c58a2b6cc841db2c011d23aa8106211fd6 (diff) | |
Merge remote-tracking branch 'github/pr/358' into v8.6
Was PR#358: Revert part of a477dc, disallow_shelved
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions