diff options
| author | Maxime Dénès | 2017-12-01 09:30:14 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-01 09:30:14 +0100 |
| commit | 565c2c2a56e118d9cf9b6b72b623055bcd68af60 (patch) | |
| tree | ec9267a3d090a256d859b6f1bf4f0ced0b09c5fd /kernel | |
| parent | 317a47249e666e2e11c6a8ac29f7c8370c861f8a (diff) | |
| parent | b16f9e8a17d2223e6045e57a11bef2aa44ffb6ff (diff) | |
Merge PR #6256: CI: better ocaml warning checks
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/nativelib.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index e9c0e171ac..4e7d6b218c 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -87,7 +87,7 @@ let call_compiler ?profile:(profile=false) ml_filename = [] in let flambda_args = - if Coq_config.caml_version_nums >= [4;3;0] then + if Coq_config.caml_version_nums >= [4;3;0] && Dynlink.is_native then (* We play safe for now, and use the native compiler with -Oclassic, however it is likely that `native_compute` users can benefit from tweaking here. |