From 35cc038e96395b0f4eaaeed3a5a48e6da2293f7e Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Fri, 4 Mar 2016 19:01:35 +0100
Subject: Fix #4607: do not read native code files if native compiler was
 disabled.

---
 library/library.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'library/library.ml')

diff --git a/library/library.ml b/library/library.ml
index 79e5792c0..ccda57c2c 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -171,9 +171,8 @@ let register_loaded_library m =
     let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in
     let f = prefix ^ "cmo" in
     let f = Dynlink.adapt_filename f in
-    (* This will not produce errors or warnings if the native compiler was
-       not enabled *)
-    Nativelib.link_library ~prefix ~dirname ~basename:f
+    if not Coq_config.no_native_compiler then
+      Nativelib.link_library ~prefix ~dirname ~basename:f
   in
   let rec aux = function
     | [] -> link m; [libname]
-- 
cgit v1.2.3