From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 27 Jul 2005 12:31:36 +0000 (+0000)
Subject: matitaMisc.ml
X-Git-Tag: V_0_7_2~37
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3cd71cda070ad61ab122f745d8cc36b17d479c93;p=helm.git

matitaMisc.ml
---

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index 9ddc268a8..82a5a521e 100644
--- 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 e3dec088b..f8a9c9bb1 100644
--- 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
 ;;