aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/library.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2014-12-16 00:06:13 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2014-12-16 00:06:13 +0100
commit8bda62e798c4e89c8c3f9406327899e394f7be0f (patch)
treeac7df2ec0c3f7b2740363428f77dadc64b774af1 /library/library.ml
parent0e730e4fa316cbfbd2d6dc60276498f57f500e0e (diff)
Fix for #3154: use CUnix.sys_command to call native compiler.
Patch by CJ on bugzilla. CUnix.sys_command doesn't rely on a shell, so extra care with cmd.exe vs sh is no longer required.
Diffstat (limited to 'library/library.ml')
-rw-r--r--library/library.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/library/library.ml b/library/library.ml
index 97c416556..4fea6b836 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -724,7 +724,7 @@ let save_library_to ?todo dir f otab =
(* Writing native code files *)
if not !Flags.no_native_compiler then
let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
- if not (Int.equal (Nativelib.compile_library dir ast fn) 0) then
+ if not (Nativelib.compile_library dir ast fn) then
msg_error (str"Could not compile the library to native code. Skipping.")
with reraise ->
let reraise = Errors.push reraise in