some prerr to better understand the mkdir -p error

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index c0277ea46c8c62d89872ea59c1998603f8eb2e9b..99fea1a32cec09944963043c058fdeda576bd9d0 100644 (file)
--- 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