From ab5201ff6902b9cf366c62e3858eba9413203b64 Mon Sep 17 00:00:00 2001
From: Nikolai Kosmatov <nikolai.kosmatov@cea.fr>
Date: Fri, 22 Feb 2019 17:15:25 +0100
Subject: [PATCH] [extlib] add recursive mkdir function (fixes #425)
---
src/kernel_services/plugin_entry_points/plugin.ml | 2 +-
src/libraries/stdlib/extlib.ml | 12 ++++++++++++
src/libraries/stdlib/extlib.mli | 11 +++++++++++
3 files changed, 24 insertions(+), 1 deletion(-)
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index bd956deba6c..1ba3d14939c 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -325,7 +325,7 @@ struct
let mk_dir d =
try
- Unix.mkdir d 0o755;
+ Extlib.mkdir ~parents:true d 0o755;
L.warning "creating %s directory `%s'" O.option_name d;
d
with Unix.Unix_error _ ->
diff --git a/src/libraries/stdlib/extlib.ml b/src/libraries/stdlib/extlib.ml
index c24744c1154..df326129833 100644
--- a/src/libraries/stdlib/extlib.ml
+++ b/src/libraries/stdlib/extlib.ml
@@ -343,6 +343,18 @@ let try_finally ~finally f x =
hence interrupting the process, might not work: child processes still need to
run some daemons, such as [flush_all] which is registered by default. *)
+let rec mkdir ?(parents=false) name perm =
+ try Unix.mkdir name perm
+ with
+ | Unix.Unix_error (Unix.ENOENT,_,_) when parents ->
+ let parent_name = Filename.dirname name in
+ if name <> parent_name then
+ begin
+ mkdir ~parents parent_name perm;
+ Unix.mkdir name perm
+ end
+ | e -> raise e
+
let pid = Unix.getpid ()
let safe_at_exit f =
at_exit
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index 389a34fc00d..89d1cc38c08 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -331,6 +331,17 @@ val try_finally: finally:(unit -> unit) -> ('a -> 'b) -> 'a -> 'b
(** System commands *)
(* ************************************************************************* *)
+val mkdir : ?parents:bool -> string -> Unix.file_perm -> unit
+ (** [mkdir ?parents name perm] creates directory [name] with permission
+ [perm]. If [parents] is true, recursively create parent directories
+ if needed. [parents] defaults to false.
+ Note that this function may create some of the parent directories
+ and then fail to create the children, e.g. if [perm] does not allow
+ user execution of the created directory. This will leave the filesystem
+ in a modified state before raising an exception.
+ @raise [Unix.Unix_error] if cannot create [name] or its parents.
+ @since Frama-C+dev *)
+
val safe_at_exit : (unit -> unit) -> unit
(** Register function to call with [Pervasives.at_exit], but only
for non-child process (fork). The order of execution is preserved
--
GitLab