aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/library.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/library/library.ml b/library/library.ml
index a8fbe0841..45fce1c26 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -169,8 +169,9 @@ 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
- if !Flags.native_compiler then
- Nativelib.link_library ~prefix ~dirname ~basename:f
+ (* This will not produce errors or warnings if the native compiler was
+ not enabled *)
+ Nativelib.link_library ~prefix ~dirname ~basename:f
in
let rec aux = function
| [] -> link m; [libname]