diff options
| author | Pierre-Marie Pédrot | 2015-05-17 16:44:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-05-17 16:44:19 +0200 |
| commit | b07c8f1224d63de6172567b04b9e008c4f18de1a (patch) | |
| tree | 268ca754f6c54552f622affb55cb8a84c738699a /lib/errors.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 'lib/errors.ml')
0 files changed, 0 insertions, 0 deletions