aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativelib.ml
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-01-08 10:46:26 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-01-08 10:46:26 +0100
commit8b0fbcc6568308794ef198f8e96093b00ba90ca4 (patch)
tree1924b3cd0aa362a89b3cc3824ba76ebe763dfbd6 /kernel/nativelib.ml
parent29d2dcb5474e4eed7e0f0d02d1e388bff53ec82d (diff)
Be more verbose about failure to compile libraries to native code.
On a machine with only 1GB of memory (e.g. in a VM), the compiler might be abruptly killed by a segfault. We were not getting any feedback in that case, making it harder to debug.
Diffstat (limited to 'kernel/nativelib.ml')
-rw-r--r--kernel/nativelib.ml12
1 files changed, 11 insertions, 1 deletions
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index b2142b43c..81470f901 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -77,7 +77,17 @@ let call_compiler ml_filename =
::include_dirs
@ ["-impl"; ml_filename] in
if !Flags.debug then Pp.msg_debug (Pp.str (compiler_name ^ " " ^ (String.concat " " args)));
- try CUnix.sys_command compiler_name args = Unix.WEXITED 0, link_filename
+ try
+ let res = CUnix.sys_command compiler_name args in
+ let res = match res with
+ | Unix.WEXITED 0 -> true
+ | Unix.WEXITED n ->
+ Pp.(msg_warning (str "command exited with status " ++ int n)); false
+ | Unix.WSIGNALED n ->
+ Pp.(msg_warning (str "command killed by signal " ++ int n)); false
+ | Unix.WSTOPPED n ->
+ Pp.(msg_warning (str "command stopped by signal " ++ int n)); false in
+ res, link_filename
with Unix.Unix_error (e,_,_) ->
Pp.(msg_warning (str (Unix.error_message e)));
false, link_filename