diff options
Diffstat (limited to 'lib/system.ml')
| -rw-r--r-- | lib/system.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/lib/system.ml b/lib/system.ml index dbab923af0..ed23bde197 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -142,7 +142,9 @@ let extern_intern ?(warn=true) magic suffix = marshal_out channel val_0; close_out channel with e -> - begin try_remove filename; raise e end + let e = Errors.push e in + let () = try_remove filename in + raise e with Sys_error s -> error ("System error: " ^ s) and intern_state paths name = try |