From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 30 Aug 2007 13:08:24 +0000 (+0000)
Subject: added an utility function
X-Git-Tag: make_still_working~6098
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f8de6ff875398b99f8fa193a1160955b46bba57b;p=helm.git

added an utility function
---

diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml
index 07886f269..d9b24c2eb 100644
--- a/helm/software/components/extlib/hExtlib.ml
+++ b/helm/software/components/extlib/hExtlib.ml
@@ -229,6 +229,13 @@ let is_regular fname =
     (Unix.stat fname).Unix.st_kind = Unix.S_REG
   with Unix.Unix_error _ -> false
 
+let is_executable fname =
+  try
+    let stat = (Unix.stat fname) in
+    stat.Unix.st_kind = Unix.S_REG &&
+    (stat.Unix.st_perm land 0o001 > 0)
+  with Unix.Unix_error _ -> false
+
 let mkdir path =
   let components = split ~sep:'/' path in
   let rec aux where = function
diff --git a/helm/software/components/extlib/hExtlib.mli b/helm/software/components/extlib/hExtlib.mli
index 99727331a..815c20526 100644
--- a/helm/software/components/extlib/hExtlib.mli
+++ b/helm/software/components/extlib/hExtlib.mli
@@ -34,6 +34,7 @@ val unopt: 'a option -> 'a  (** @raise Failure *)
 val is_dir: string -> bool  (** @return true if file is a directory *)
 val writable_dir: string -> bool  (** @return true if the directory is writable *)
 val is_regular: string -> bool  (** @return true if file is a regular file *)
+val is_executable: string -> bool  (** @return true if file is executable *)
 val mkdir: string -> unit (** create dir and parents. @raise Failure *)
 val tilde_expand: string -> string  (** bash-like (head) tilde expansion *)
 val safe_remove: string -> unit (** removes a file if it exists *)