diff options
Diffstat (limited to 'lib/system.ml')
| -rw-r--r-- | lib/system.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/system.ml b/lib/system.ml index 0c4e892b9..1d1968a7c 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -200,7 +200,7 @@ let extern_intern ?(warn=true) magic = with reraise -> let reraise = Errors.push reraise in let () = try_remove filename in - raise reraise + iraise reraise with Sys_error s -> error ("System error: " ^ s) and intern_state paths name = try |