diff options
| author | Pierre-Marie Pédrot | 2015-05-05 00:20:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-05-05 00:20:54 +0200 |
| commit | 34e6a7149a69791cc736bdd9b2b909be9f21ec8f (patch) | |
| tree | f33a4ed37d7fff96df7a720fe6146ecce56aba81 /lib/system.ml | |
| parent | 72644c7f7b3f0fcc56779acfcfa4bfc9f041ebde (diff) | |
| parent | df54c829a4c06a93de47df4e8ccc441721360da8 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'lib/system.ml')
| -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 70f5904629..e4a60eccb7 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -159,7 +159,8 @@ let is_in_system_path filename = let open_trapping_failure name = try open_out_bin name - with e when Errors.noncritical e -> error ("Can't open " ^ name) + with e when Errors.noncritical e -> + errorlabstrm "System.open" (str "Can't open " ++ str name) let try_remove filename = try Sys.remove filename @@ -167,7 +168,8 @@ let try_remove filename = msg_warning (str"Could not remove file " ++ str filename ++ str" which is corrupted!") -let error_corrupted file s = error (file ^": " ^ s ^ ". Try to rebuild it.") +let error_corrupted file s = + errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.") let input_binary_int f ch = try input_binary_int ch @@ -242,7 +244,8 @@ let extern_intern ?(warn=true) magic = let reraise = Errors.push reraise in let () = try_remove filename in iraise reraise - with Sys_error s -> error ("System error: " ^ s) + with Sys_error s -> + errorlabstrm "System.extern_state" (str "System error: " ++ str s) and intern_state paths name = try let _,filename = find_file_in_path ~warn paths name in @@ -251,7 +254,7 @@ let extern_intern ?(warn=true) magic = close_in channel; v with Sys_error s -> - error("System error: " ^ s) + errorlabstrm "System.intern_state" (str "System error: " ++ str s) in (extern_state,intern_state) |