]> matita.cs.unibo.it Git - helm.git/commitdiff
we chmod the created directories to override the umask settings
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 23 Sep 2007 19:57:56 +0000 (19:57 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 23 Sep 2007 19:57:56 +0000 (19:57 +0000)
helm/software/components/extlib/hExtlib.ml

index bf3bb2574b7608327129d235974d74f7c4d0f48f..9e2277b43041b9f551a67d7ad422369475818d2b 100644 (file)
@@ -236,6 +236,9 @@ let is_executable fname =
     (stat.Unix.st_perm land 0o001 > 0)
   with Unix.Unix_error _ -> false
 
+let chmod mode filename =
+   Unix.chmod filename mode
+
 let mkdir path =
   let components = split ~sep:'/' path in
   let rec aux where = function
@@ -244,21 +247,18 @@ let mkdir path =
         let path =
           if where = "" then piece else where ^ "/" ^ piece in
         (try
-          Unix.mkdir path 0o775
+          Unix.mkdir path 0o755; chmod 0o2775 path 
         with 
         | Unix.Unix_error (Unix.EEXIST,_,_) -> ()
         | Unix.Unix_error (e,_,_) -> 
             raise 
               (Failure 
-                ("Unix.mkdir " ^ path ^ " 0o775 :" ^ (Unix.error_message e))));
+                ("Unix.mkdir " ^ path ^ " 0o2775 :" ^ (Unix.error_message e))));
         aux path tl
   in
   let where = if path.[0] = '/' then "/" else "" in
   aux where components
 
-let chmod mode filename =
-   Unix.chmod filename mode
-
 (** {2 Filesystem} *)
 
 let input_file fname =