From 29d2dcb5474e4eed7e0f0d02d1e388bff53ec82d Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 7 Jan 2016 17:21:54 +0100
Subject: Fix a misleading comment for substn_vars

---
 kernel/vars.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/vars.mli b/kernel/vars.mli
index c0fbeeb6e6..9f034b288a 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -65,7 +65,7 @@ val subst_var : Id.t -> constr -> constr
    if two names are identical, the one of least indice is kept *)
 val subst_vars : Id.t list -> constr -> constr
 
-(** [substn_vars n [id1;...;idn] t] substitute [VAR idj] by [Rel j+n-1] in [t]
+(** [substn_vars n [id1;...;idk] t] substitute [VAR idj] by [Rel j+n-1] in [t]
    if two names are identical, the one of least indice is kept *)
 val substn_vars : int -> Id.t list -> constr -> constr
 
-- 
cgit v1.2.3


From 8b0fbcc6568308794ef198f8e96093b00ba90ca4 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 8 Jan 2016 10:46:26 +0100
Subject: 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.
---
 kernel/nativelib.ml | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index b2142b43c7..81470f9015 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
-- 
cgit v1.2.3