From 6acf543800fe176ca7d47ef7165ebc14588efb6f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 29 Apr 2014 14:41:49 -0400
Subject: Native compiler: hide compiled files in a .coq-native subdirectory.

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

(limited to 'library')

diff --git a/library/library.ml b/library/library.ml
index fd391344c1..8521325b04 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -107,7 +107,7 @@ let register_loaded_library m =
     let f = prefix ^ "cmo" in
     let f = Dynlink.adapt_filename f in
     if not !Flags.no_native_compiler then
-      Nativelib.call_linker ~fatal:false prefix (Filename.concat dirname f) None
+      Nativelib.link_library ~prefix ~dirname ~basename:f
   in
   let rec aux = function
     | [] -> link m; [m]
@@ -760,7 +760,7 @@ let save_library_to ?todo dir f =
     if not !Flags.no_native_compiler then
       let lp = Loadpath.get_accessible_paths () in
       let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
-      if not (Int.equal (Nativelibrary.compile_library dir ast lp fn) 0) then
+      if not (Int.equal (Nativelib.compile_library dir ast lp fn) 0) then
         msg_error (str"Could not compile the library to native code. Skipping.")
    with reraise ->
     let reraise = Errors.push reraise in
-- 
cgit v1.2.3