From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 20 Mar 2013 18:43:07 +0000 (+0000)
Subject: - probe: recursive removal of empty directories
X-Git-Tag: make_still_working~1203
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=85a33f6b6de49ad8076753643df41f39bbedf802;p=helm.git

- probe: recursive removal of empty directories
- matitadep: improved parsing of input
---

diff --git a/matita/components/binaries/matitadep/matitadep.ml b/matita/components/binaries/matitadep/matitadep.ml
index da82b9fc1..de8f3d65d 100644
--- a/matita/components/binaries/matitadep/matitadep.ml
+++ b/matita/components/binaries/matitadep/matitadep.ml
@@ -47,7 +47,7 @@ let check () =
    Hashtbl.iter iter graph 
 
 let rec read ich = 
-   let _ = Scanf.fscanf ich "%s@:include \"%s@\". " init in
+   let _ = Scanf.sscanf (input_line ich) "%s@:include \"%s@\"." init in
    read ich
    
 let _ =
diff --git a/matita/components/binaries/probe/matitaRemove.ml b/matita/components/binaries/probe/matitaRemove.ml
index 1ef87a5ca..0ad0cd1d4 100644
--- a/matita/components/binaries/probe/matitaRemove.ml
+++ b/matita/components/binaries/probe/matitaRemove.ml
@@ -17,10 +17,14 @@ module U = Unix
 module O = Options
 
 let remove_dir dir =
+   let map name = Y.remove (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 rmdir dir with U.Unix_error _ -> ()
    end
 
 let objects () =