universes are saved to disk

[helm.git] / helm / matita / matitaMisc.ml

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index c67602dbac3065f00745a9c4aea2fe1fae0c5a55..56cb4a29535f1734b5db12cc3c09410971be69ed 100644 (file)
--- a/helm/matita/matitaMisc.ml
+++ b/helm/matita/matitaMisc.ml
@@ -126,7 +126,10 @@ let mkdir path =
           Unix.mkdir path 0o755
         with 
         | Unix.Unix_error (Unix.EEXIST,_,_) -> ()
-        | Unix.Unix_error (e,_,_) -> raise (Failure (Unix.error_message e)));
+        | Unix.Unix_error (e,_,_) -> 
+            raise 
+              (Failure 
+                ("Unix.mkdir " ^ path ^ " 0o755 :" ^ (Unix.error_message e))));
         aux path tl
   in
   aux "" components