projects
/
helm.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
789bd6e
)
use safe_remove to remove files instead of Unix.unlink
author
Stefano Zacchiroli
<zack@upsilon.cc>
Tue, 19 Jul 2005 17:24:06 +0000
(17:24 +0000)
committer
Stefano Zacchiroli
<zack@upsilon.cc>
Tue, 19 Jul 2005 17:24:06 +0000
(17:24 +0000)
helm/matita/matitaclean.ml
patch
|
blob
|
history
diff --git
a/helm/matita/matitaclean.ml
b/helm/matita/matitaclean.ml
index d37f0bfdd99aa82ac00cf41e1ee552ab82d131aa..89b602735704426403882177f64c4d8ee0415466 100644
(file)
--- a/
helm/matita/matitaclean.ml
+++ b/
helm/matita/matitaclean.ml
@@
-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
+