From 226a7c21173a8e93edaf509513834231c1847464 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 23 Apr 2020 18:23:14 +0200
Subject: [PATCH] [kernel] Avoid to create an already existing directory. Abort
if a file with same path already exists.
---
.../plugin_entry_points/plugin.ml | 19 ++++++++++++++++---
1 file changed, 16 insertions(+), 3 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index 3e4c529f2b6..40e1c3b1699 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -395,8 +395,19 @@ struct
| `Normalize_only ->
filepath
| `Create_path ->
- ignore (mk_dir (filepath :> string));
- filepath
+ begin
+ (try
+ if not (Sys.is_directory (filepath :> string))
+ then
+ (* [filepath] already exists, and it is a file. *)
+ L.abort
+ "cannot create directory as file %a already exists"
+ Datatype.Filepath.pretty filepath
+ with Sys_error _ ->
+ (* [filepath] does not exist: create the directory path. *)
+ ignore (mk_dir (filepath :> string)));
+ filepath
+ end
end
let get_file ?(mode=`Normalize_only) s =
@@ -448,7 +459,9 @@ struct
end)
let () =
if is_kernel ()
- then Journal.get_session_file := (fun s -> Session.get_file s)
+ then
+ Journal.get_session_file :=
+ (fun s -> Session.get_file ~mode:`Create_path s)
module Config =
Make_specific_dir
--
GitLab