From 4da752354f04090cc69c3d85a34059b8d9e28be2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 17 Jul 2018 13:51:59 +0200
Subject: Properly disable native compilation when -native-compiler is unset.

There was a function used by the pretyper that did not check that the flag was
set, leading to native compilation even when the configure flag was off.
---
 kernel/nativelib.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/nativelib.ml')

diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 31ad364911..f784509b6f 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -67,6 +67,7 @@ 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
-- 
cgit v1.2.3