diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-05-17 16:44:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-05-17 16:44:19 +0200 |
| commit | b07c8f1224d63de6172567b04b9e008c4f18de1a (patch) | |
| tree | 268ca754f6c54552f622affb55cb8a84c738699a /kernel/nativelib.ml | |
| parent | b14d88c8cd17ad524898b31c1772a0e8f70f19f8 (diff) | |
Fixing bug #4201: The native compiler is not race-free.
Instead of checking if the native compiler directory exists before creating it,
we simply create it by default and catch the potential exception due to its
presence.
Diffstat (limited to 'kernel/nativelib.ml')
| -rw-r--r-- | kernel/nativelib.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 605c1225c..29b6bf6de 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -94,7 +94,10 @@ let compile_library dir code fn = let basename = Filename.basename fn in let dirname = Filename.dirname fn in let dirname = dirname / output_dir in - if not (Sys.file_exists dirname) then Unix.mkdir dirname 0o755; + let () = + try Unix.mkdir dirname 0o755 + with Unix.Unix_error (Unix.EEXIST, _, _) -> () + in let fn = dirname / basename in write_ml_code fn ~header code; let r = fst (call_compiler fn) in |