diff options
| author | Alec Faithfull | 2015-10-06 13:50:59 +0200 |
|---|---|---|
| committer | Alec Faithfull | 2015-10-09 10:53:29 +0200 |
| commit | b2007e86b4a28570eee52439ad8b9fee603443b8 (patch) | |
| tree | 2d1fd2cb98fa75d589fb8425fed1339ce2a7514d /kernel/nativecode.ml | |
| parent | 73daf37ccc7a44cd29c9b67405111756c75cb26a (diff) | |
STM: Pass exception information to unreachable_state_hook functions
This lets hooks treat different exceptions in different ways; in
particular, user interrupts can now be safely ignored
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions