aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
authorMaxime Dénès2020-04-01 11:09:13 +0200
committerMaxime Dénès2020-04-01 11:09:13 +0200
commit828b79f744ffc1f292a77a80553906544c1c0cfb (patch)
treef267db7f0d4895e14548281d59e61cd11379ebf4 /vernac
parenteacddd7054ddc04eafc8292ae80be84649b940d1 (diff)
parentacba2419a4cebb2b55bad2aefa2062640ffe8828 (diff)
Merge PR #11306: Centralize the flag handling native compilation.
Ack-by: SkySkimmer Reviewed-by: maximedenes
Diffstat (limited to 'vernac')
-rw-r--r--vernac/library.ml7
1 files changed, 4 insertions, 3 deletions
diff --git a/vernac/library.ml b/vernac/library.ml
index 7c629b08e7..1b0bd4c0f7 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -155,11 +155,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;