diff options
| author | Matthieu Sozeau | 2019-01-07 13:46:42 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-01-07 13:46:42 +0100 |
| commit | ffcb5526d33c1eaa2016dd3af9e3dffd932b7874 (patch) | |
| tree | 1e567b2f5dd90f9329a42ff2dcb0407277af5bd7 /kernel/type_errors.mli | |
| parent | 8c040974facb733682d24c488dc89941671f4ab7 (diff) | |
| parent | 0703cd1bbe5aab7e584d2293fe76c5f6ac4fe08c (diff) | |
Merge PR #8373: Fixes #8369: Not_found in printing message about an unresolved subevar.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions