aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/system.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/system.ml')
-rw-r--r--lib/system.ml11
1 files changed, 7 insertions, 4 deletions
diff --git a/lib/system.ml b/lib/system.ml
index 73095f9cd..d1cdd8efc 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -118,7 +118,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
@@ -126,7 +127,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
@@ -201,7 +203,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
@@ -210,7 +213,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)