From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 22 Jul 2005 11:46:00 +0000 (+0000)
Subject: some prerr to better understand the mkdir -p error
X-Git-Tag: V_0_7_2~109
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2a953f2a05308ee417f63dceb29e027c527d4e17;p=helm.git

some prerr to better understand the mkdir -p error
---

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index c0277ea46..99fea1a32 100644
--- a/helm/matita/matitaMisc.ml
+++ b/helm/matita/matitaMisc.ml
@@ -177,10 +177,21 @@ let singleton f =
 let mkdir d =
   let errmsg = sprintf "Unable to create directory \"%s\"" d in
   try
-    (match Unix.system ("mkdir -p " ^ d) with
+    let dir = "mkdir -p " ^ d in 
+    (match Unix.system dir with
     | Unix.WEXITED 0 -> ()
-    | _ -> failwith errmsg)
-  with Unix.Unix_error _ -> failwith errmsg
+    | Unix.WEXITED n -> 
+        MatitaLog.error ("'mkdir -p " ^ dir ^ "' failed with "^string_of_int n);
+        failwith errmsg
+    | Unix.WSIGNALED s 
+    | Unix.WSTOPPED s -> 
+        MatitaLog.error 
+          ("'mkdir -p " ^ dir ^ "' signaled with " ^ string_of_int s);
+        failwith errmsg)
+  with Unix.Unix_error _ as exc -> 
+    MatitaLog.error 
+      ("Unix error in makigin dir " ^ (MatitaExcPp.to_string exc));
+    failwith errmsg
 
 let get_proof_status status =
   match status.proof_status with