Fix #4607: do not read native code files if native compiler was disabled.

1 files changed, 2 insertions, 3 deletions

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]