X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fprobe%2FmatitaRemove.ml;h=72624f0f09b05f155d8b5727e1ef1fe3777238d8;hb=50001ac0b45a3f6376e8cbfd9200149a01d68148;hp=87be455213258ebe0cc6d65f18b77ebe41eabb91;hpb=c559209567ff7ec5e4d3de7fef431398f9ba2559;p=helm.git diff --git a/matita/components/binaries/probe/matitaRemove.ml b/matita/components/binaries/probe/matitaRemove.ml index 87be45521..72624f0f0 100644 --- a/matita/components/binaries/probe/matitaRemove.ml +++ b/matita/components/binaries/probe/matitaRemove.ml @@ -16,8 +16,11 @@ module U = Unix module O = Options -let remove_dir dir = - let map name = Y.remove (F.concat dir name) in +let rec remove_obj name = + try Y.remove name with Sys_error _ -> remove_dir name + +and remove_dir dir = + let map name = remove_obj (F.concat dir name) in let rec rmdir dir = U.rmdir dir; (* Sys.remove does not seem to remove empty directories *) rmdir (F.dirname dir) @@ -28,8 +31,4 @@ let remove_dir dir = end let objects () = - let map name = - Y.remove name; - remove_dir (F.chop_extension name) - in - List.iter map !O.remove + List.iter remove_obj !O.remove