matitaMisc.ml

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index 9ddc268a815265d336cd43348b16caa8b6f5d451..82a5a521e57173899b8d6201043b9f78a495b0a7 100644 (file)
--- a/helm/matita/matitaMisc.ml
+++ b/helm/matita/matitaMisc.ml
@@ -121,7 +121,7 @@ let mkdir path =
     | piece::tl -> 
         let path = where ^ "/" ^ piece in
         (try
-          Unix.mkdir path 755
+          Unix.mkdir path 0o755
         with 
         | Unix.Unix_error (Unix.EEXIST,_,_) -> ()
         | Unix.Unix_error (e,_,_) -> raise (Failure (Unix.error_message e)));

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index e3dec088b4034ab8331e578814873c567dbe527f..f8a9c9bb132a3b23c0596d4b1778a701f06836d0 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -171,7 +171,7 @@ let eval_with_engine guistuff status user_goal parsed_text st =
         | `NO -> raise exc
         | `CANCEL -> do_nothing ())
       in
-      let handle_withoud_devel filename =
+      let handle_without_devel filename =
         let title = "Unable to include " ^ what in
         let message = 
          what ^ " is <b>not</b> handled by a development.\n" ^
@@ -189,11 +189,11 @@ let eval_with_engine guistuff status user_goal parsed_text st =
         | `CANCEL -> do_nothing())
       in
       match guistuff.filenamedata with
-      | None,None -> handle_withoud_devel None
+      | None,None -> handle_without_devel None
       | None,Some d -> handle_with_devel d
       | Some f,_ ->
           match MatitamakeLib.development_for_dir (Filename.dirname f) with
-          | None -> handle_withoud_devel (Some f)
+          | None -> handle_without_devel (Some f)
           | Some d -> handle_with_devel d
 ;;