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

1 files changed, 7 insertions, 6 deletions

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 =