diff options
| author | Guillaume Melquiond | 2015-04-02 13:16:17 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-04-02 14:14:16 +0200 |
| commit | 27a87e4487c8b926aa0ed6c0ab65333d4ef5c3bc (patch) | |
| tree | 5fe2cb6313f59d80c6343ec45204abca8eb63287 /kernel/type_errors.mli | |
| parent | 4de4ab77ab6d9bb72a41c3fee3920a4c1b7a9bbc (diff) | |
Display the proper error message when Require fails to find a library.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions