aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelib.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-11-05 14:25:10 +0100
committerPierre-Marie Pédrot2018-11-05 14:25:10 +0100
commitea678521c9eda7acde3a0276e0cec0931dbc6416 (patch)
treecbc2baf5777992a7e81e24a662dfce5db311d6a2 /kernel/nativelib.ml
parentafc3e334c02cbbbe395387ff7110a296dce6c9f6 (diff)
parente2e7fea91f3af5dcf62052078da65489b796e9e2 (diff)
Merge PR #8870: Pass native and VM flags to the kernel through environment
Diffstat (limited to 'kernel/nativelib.ml')
-rw-r--r--kernel/nativelib.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index d294f2060e..833e4082f0 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -66,7 +66,6 @@ let warn_native_compiler_failed =
CWarnings.create ~name:"native-compiler-failed" ~category:"native-compiler" print
let call_compiler ?profile:(profile=false) ml_filename =
- let () = assert Coq_config.native_compiler in
let load_path = !get_load_paths () in
let load_path = List.map (fun dn -> dn / output_dir) load_path in
let include_dirs = List.flatten (List.map (fun x -> ["-I"; x]) (include_dirs () @ load_path)) in