diff options
author | Eelco Dolstra <edolstra@gmail.com> | 2017-06-20 12:11:22 +0200 |
---|---|---|
committer | Eelco Dolstra <edolstra@gmail.com> | 2017-06-20 12:13:17 +0200 |
commit | c7346a275c4cdcb59b3961241ddc52b79452d716 (patch) | |
tree | 088827d50b7373ec5bd4ce1cd8403c07d01d2777 /local.mk | |
parent | 04ed11a978bf70e04042df95f8b125c2977e070d (diff) |
Restore thunks on any exception
There's no reason to restrict this to Error exceptions. This shouldn't
matter to #1407 since the repl doesn't catch non-Error exceptions
anyway, but you never know...
Diffstat (limited to 'local.mk')
0 files changed, 0 insertions, 0 deletions