diff options
| author | Maxime Dénès | 2014-04-29 14:41:49 -0400 |
|---|---|---|
| committer | Maxime Dénès | 2014-04-29 14:41:49 -0400 |
| commit | 6acf543800fe176ca7d47ef7165ebc14588efb6f (patch) | |
| tree | 1bf524ee47195cc4d3ebdd48113aaeeaf1bc5c1d /library | |
| parent | 3b176883b7fcd9af6881ae1049bbd078c8d19577 (diff) | |
Native compiler: hide compiled files in a .coq-native subdirectory.
Diffstat (limited to 'library')
| -rw-r--r-- | library/library.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |