X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fprobe%2FmatitaRemove.ml;h=b34cfc35729456b9cea64e8cc0e3d4c5bc7c1c81;hb=076439def28e649ec384fae038ed021dadd5f75c;hp=1ef87a5ca16efd829c127ca20c104b3760cf64fc;hpb=8ff4315142253a1a0478b67c07dddf70c36f50cd;p=helm.git

diff --git a/matita/components/binaries/probe/matitaRemove.ml b/matita/components/binaries/probe/matitaRemove.ml
index 1ef87a5ca..b34cfc357 100644
--- a/matita/components/binaries/probe/matitaRemove.ml
+++ b/matita/components/binaries/probe/matitaRemove.ml
@@ -1,12 +1,12 @@
 (*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.      
-     \ /   This software is distributed as is, NO WARRANTY.     
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department, University of Bologna, Italy.
+    ||I||
+    ||T||  HELM is free software; you can redistribute it and/or
+    ||A||  modify it under the terms of the GNU General Public License
+    \   /  version 2 or (at your option) any later version.
+     \ /   This software is distributed as is, NO WARRANTY.
       V_______________________________________________________________ *)
 
 module A = Array
@@ -16,16 +16,19 @@ module U = Unix
 
 module O = Options
 
-let remove_dir dir =
+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
-      let map name = Y.remove (F.concat dir name) in
-      A.iter map (Y.readdir dir);
-      U.rmdir dir (* Sys.remove does not seem to remove empty directories *)
+      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