]> matita.cs.unibo.it Git - helm.git/commitdiff
bugfix: mkdir now works also for realtive directories
authorStefano Zacchiroli <zack@upsilon.cc>
Fri, 3 Feb 2006 15:14:27 +0000 (15:14 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Fri, 3 Feb 2006 15:14:27 +0000 (15:14 +0000)
helm/ocaml/extlib/hExtlib.ml

index 15a459cdc0f1243c44d0017e6e1bffab0f5c0506..5f96e0f84e7fad3237394a835e68dfafe1311b31 100644 (file)
 
 (** PROFILING *)
 
-(* we should use a key in te registry, but we can't see the registry.. *)
-let profiling_enabled = true
+let profiling_enabled = ComponentsConf.profiling
 
 let profiling_printings = ref (fun () -> true)
 let set_profiling_printings f = profiling_printings := f
 
 type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b }
 let profile ?(enable = true) =
- if profiling_enabled  && enable then
+ if profiling_enabled && enable then
   function s ->
    let total = ref 0.0 in
    let profile f x =
@@ -163,7 +162,8 @@ let mkdir path =
   let rec aux where = function
     | [] -> ()
     | piece::tl -> 
-        let path = where ^ "/" ^ piece in
+        let path =
+          if where = "" then piece else where ^ "/" ^ piece in
         (try
           Unix.mkdir path 0o755
         with 
@@ -174,7 +174,8 @@ let mkdir path =
                 ("Unix.mkdir " ^ path ^ " 0o755 :" ^ (Unix.error_message e))));
         aux path tl
   in
-  aux "" components
+  let where = if path.[0] = '/' then "/" else "" in
+  aux where components
 
 (** {2 Filesystem} *)