Restrict (try...with...) to avoid catching critical exn (part 8)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16284 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 8 insertions, 6 deletions

diff --git a/lib/system.ml b/lib/system.ml
index 41201bd2d3..a72958b99b 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -105,12 +105,14 @@ let is_in_system_path filename =
   is_in_path lpath filename
 
 let open_trapping_failure name =
-  try open_out_bin name with _ -> error ("Can't open " ^ name)
+  try open_out_bin name
+  with e when Errors.noncritical e -> error ("Can't open " ^ name)
 
 let try_remove filename =
   try Sys.remove filename
-  with _ -> msg_warning
-    (str"Could not remove file " ++ str filename ++ str" which is corrupted!")
+  with e when Errors.noncritical e ->
+    msg_warning
+      (str"Could not remove file " ++ str filename ++ str" which is corrupted!")
 
 let marshal_out ch v = Marshal.to_channel ch v []
 let marshal_in filename ch =
@@ -143,10 +145,10 @@ let extern_intern ?(warn=true) magic suffix =
       try
         marshal_out channel val_0;
         close_out channel
-      with e ->
-	let e = Errors.push e in
+      with reraise ->
+	let reraise = Errors.push reraise in
         let () = try_remove filename in
-        raise e
+        raise reraise
     with Sys_error s -> error ("System error: " ^ s)
   and intern_state paths name =
     try