diff options
| author | Pierre-Marie Pédrot | 2015-05-18 17:47:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-05-18 19:04:32 +0200 |
| commit | ea3909466eaaf86ff212c0a002e5df11e4a979f5 (patch) | |
| tree | 2fd23c2ffa95c3bcfcd5c3e15404716dbc4df283 /kernel/nativecode.ml | |
| parent | b994685d85d30f0db8ee0ec10f802f6bf3797e4b (diff) | |
The Fail command does not catch uncaught exception anomalies anymore.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions