diff options
| author | Emilio Jesus Gallego Arias | 2018-02-09 23:33:48 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-02-09 23:52:19 +0100 |
| commit | 250dc1f50e17240df158978159f408fe9231f410 (patch) | |
| tree | e0a1d97659cfd6a66ef9507d5a5b56895f5c300b /kernel/type_errors.ml | |
| parent | 47e43e229ab02a4dedc2405fed3960a4bf476b58 (diff) | |
[nativecomp] Remove ad-hoc handling of Dynlink exception.
Instead, we properly register a printer for such exception and update
the code.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions