]> matita.cs.unibo.it Git - helm.git/commitdiff
use safe_remove to remove files instead of Unix.unlink
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 19 Jul 2005 17:24:06 +0000 (17:24 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 19 Jul 2005 17:24:06 +0000 (17:24 +0000)
helm/matita/matitaclean.ml

index d37f0bfdd99aa82ac00cf41e1ee552ab82d131aa..89b602735704426403882177f64c4d8ee0415466 100644 (file)
@@ -78,7 +78,5 @@ let _ =
     Invalid_argument _ -> usage ());
   main !uris_to_remove;
   let moos = List.map MatitaMisc.obj_file_of_script !files_to_remove in
-  List.iter
-    (fun s -> try Unix.unlink s with Unix.Unix_error _ -> ()) 
-    moos
-    
+  List.iter MatitaMisc.safe_remove moos
+