From 164c6861860e6b52818c031f901ffeff91fca16a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 26 Jan 2016 16:56:33 +0100
Subject: Imported Upstream version 8.5

---
 kernel/nativelib.ml | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

(limited to 'kernel/nativelib.ml')

diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index b2142b43..948989fd 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -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