diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-06-16 10:03:29 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-06-16 10:03:29 +0200 |
| commit | f1ecf669d82c8b6d05068e12f96f993982ecb533 (patch) | |
| tree | e9750314c2b28d3416ec420e9e3f5b9e21033d82 /kernel/nativelib.ml | |
| parent | 5e5a4c9a54903c4a7a4bdcf5e8cec5768f9e3d33 (diff) | |
Preemptively remove files from native compilation.
Ocaml does not remove the .cmi file if compilation fails, thus causing
subsequent native compilations to fail due to mismatching interfaces.
For the sake of homogeneity, also remove the .cmo/.cmxs file along the way.
Diffstat (limited to 'kernel/nativelib.ml')
| -rw-r--r-- | kernel/nativelib.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index b877dda8f..0ad345795 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -67,6 +67,9 @@ let call_compiler ml_filename = let f = Filename.chop_extension ml_filename in let link_filename = f ^ ".cmo" in let link_filename = Dynlink.adapt_filename link_filename in + let remove f = if Sys.file_exists f then Sys.remove f in + remove link_filename; + remove (f ^ ".cmi"); let comp_cmd = Format.sprintf "%s -%s -o %s -rectypes -w a -I %s -impl %s" compiler_name (if Dynlink.is_native then "shared" else "c") |