From 36701f1900c8247d76436f2cf7ee09865b45ce3f Mon Sep 17 00:00:00 2001
From: barras
Date: Fri, 9 Mar 2001 16:11:48 +0000
Subject: protection contre certaines exceptions levees par marshal_{in,out}
 possibilite de declarer une def syntaxique comme infix (utilise par FTA)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1442 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/library.ml | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

(limited to 'library')

diff --git a/library/library.ml b/library/library.ml
index ba41615a9e..e58f716597 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -210,12 +210,13 @@ let save_module_to process s f =
     md_nametab = process seg;
     md_deps = current_imports () } in
   let (f',ch) = raw_extern_module f in
-  System.marshal_out ch md;
-  flush ch;
-  let di = Digest.file f' in
-  System.marshal_out ch di;
-  close_out ch
-
+  try
+    System.marshal_out ch md;
+    flush ch;
+    let di = Digest.file f' in
+    System.marshal_out ch di;
+    close_out ch
+  with e -> (warning ("Removed file "^f');close_out ch; Sys.remove f'; raise e)
 (*s Iterators. *)
 
 let fold_all_segments insec f x =
-- 
cgit v1.2.3