diff options
Diffstat (limited to 'clib/cUnix.ml')
| -rw-r--r-- | clib/cUnix.ml | 21 |
1 files changed, 19 insertions, 2 deletions
diff --git a/clib/cUnix.ml b/clib/cUnix.ml index c5f6bebb8e..75ed73540e 100644 --- a/clib/cUnix.ml +++ b/clib/cUnix.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -140,3 +140,20 @@ let same_file f1 = Unix.Unix_error _ -> false) with Unix.Unix_error _ -> (fun _ -> false) + +(* Copied from ocaml filename.ml *) +let prng = lazy(Random.State.make_self_init ()) + +let temp_file_name temp_dir prefix suffix = + let rnd = (Random.State.bits (Lazy.force prng)) land 0xFFFFFF in + Filename.concat temp_dir (Printf.sprintf "%s%06x%s" prefix rnd suffix) + +let mktemp_dir ?(temp_dir=Filename.get_temp_dir_name()) prefix suffix = + let rec try_name counter = + let name = temp_file_name temp_dir prefix suffix in + match Unix.mkdir name 0o700 with + | () -> name + | exception (Sys_error _ as e) -> + if counter >= 1000 then raise e else try_name (counter + 1) + in + try_name 0 |