diff options
Diffstat (limited to 'library/library.ml')
| -rw-r--r-- | library/library.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/library/library.ml b/library/library.ml index 37dadadb76..04e38296d9 100644 --- a/library/library.ml +++ b/library/library.ml @@ -718,8 +718,7 @@ let save_library_to ?todo ~output_native_objects dir f otab = (* Writing native code files *) if output_native_objects then let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in - if not (Nativelib.compile_library dir ast fn) then - user_err Pp.(str "Could not compile the library to native code.") + Nativelib.compile_library dir ast fn with reraise -> let reraise = CErrors.push reraise in let () = Feedback.msg_warning (str "Removed file " ++ str f') in |