diff options
| author | Enrico Tassi | 2018-11-20 17:26:44 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2018-11-20 17:26:44 +0100 |
| commit | fc9c25270f22e2e34c45d47f0362d543c1bd2421 (patch) | |
| tree | 214c32650c19b607eac9e72a6a512818955ffd44 /kernel/type_errors.mli | |
| parent | 100744560bd04184eb7e6c3fa36e8533e468e700 (diff) | |
| parent | f0cb72dded093175feab3f19aac63fab46999e0a (diff) | |
Merge PR #8959: [dune] [ide] Install data files.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions