diff options
| -rw-r--r-- | lib/system.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/lib/system.ml b/lib/system.ml index 28af1ee40f..015124e5bc 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -134,10 +134,13 @@ let raw_extern_intern magic = output_binary_int channel magic; filename, channel and intern_state filename = - let channel = open_in_bin filename in - if not (Int.equal (input_binary_int channel) magic) then - raise (Bad_magic_number filename); - channel + try + let channel = open_in_bin filename in + if not (Int.equal (input_binary_int channel) magic) then + raise (Bad_magic_number filename); + channel + with End_of_file | Failure _ | Sys_error _ -> + error_corrupted filename in (extern_state,intern_state) |