diff options
| author | Emilio Jesus Gallego Arias | 2020-01-30 23:36:19 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-01-30 23:36:19 +0100 |
| commit | 173a2d8b0fba1a85b618654151af04b5decf9bac (patch) | |
| tree | 8f7385dbc348bed11568414729ec4e1f65a295e4 /kernel/type_errors.mli | |
| parent | 869f731439b7fe034067bb550b60713b9b790f5b (diff) | |
[exn] Don't reraise in exception printers
This behaviour seems a bit dubious and it is indeed not needed, also
such re-raises seem like they will mess with the backtrace.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions