diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/library.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/vernac/library.ml b/vernac/library.ml index 244424de6b..6ed38410c4 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -159,11 +159,12 @@ 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 Coq_config.native_compiler then - Nativelib.link_library (Global.env()) ~prefix ~dirname ~basename:f + Nativelib.link_library (Global.env()) ~prefix ~dirname ~basename:f in let rec aux = function - | [] -> link (); [libname] + | [] -> + let () = if Flags.get_native_compiler () then link () in + [libname] | m'::_ as l when DirPath.equal m' libname -> l | m'::l' -> m' :: aux l' in libraries_loaded_list := aux !libraries_loaded_list; |