diff options
| author | Maxime Dénès | 2019-01-17 15:48:55 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-17 15:48:55 +0100 |
| commit | 84e919a0969ff8dce44c6c5fb8bfd248f652e841 (patch) | |
| tree | b5ab6408299bfc9ad13fda3edb8581b287e7bf86 /kernel/type_errors.mli | |
| parent | a55679c7ed863a3a0917ef52b9ccf9da248dcf5d (diff) | |
| parent | e323a36fd79000df30bbac9911d00ca80589fb23 (diff) | |
Merge PR #9242: merge-pr: add reviewer info to commit message
Reviewed-by: maximedenes
Ack-by: ejgallego
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions