- xoa: the definitions file now includes the notations file

[helm.git] / matita / components / binaries / probe / matitaRemove.ml

diff --git a/matita/components/binaries/probe/matitaRemove.ml b/matita/components/binaries/probe/matitaRemove.ml
index 0ad0cd1d4b3fcc67fda75c2d1f101b138dad5394..72624f0f09b05f155d8b5727e1ef1fe3777238d8 100644 (file)
--- a/matita/components/binaries/probe/matitaRemove.ml
+++ b/matita/components/binaries/probe/matitaRemove.ml
@@ -16,20 +16,19 @@ 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)
    in
    if Y.file_exists dir then begin
-      A.iter map (Y.readdir dir);
-      try rmdir dir with U.Unix_error _ -> ()
+      try A.iter map (Y.readdir dir); rmdir dir
+      with U.Unix_error _ -> ()
    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