# HG changeset patch
# User wenzelm
# Date 1586788376 -7200
# Node ID 34de8369c2902360968643eed297d73eec6c09e5
# Parent  1dd514c8c1df1f1b88ef1509087dd674be3240e3
tuned message;

diff -r 1dd514c8c1df -r 34de8369c290 src/Pure/System/process_result.scala
--- a/src/Pure/System/process_result.scala	Mon Apr 13 16:16:22 2020 +0200
+++ b/src/Pure/System/process_result.scala	Mon Apr 13 16:32:56 2020 +0200
@@ -8,7 +8,23 @@
 
 object Process_Result
 {
-  def print_return_code(rc: Int): String = "Return code: " + rc
+  val return_code_text: Map[Int, String] =
+    Map(0 -> "OK",
+      1 -> "ERROR",
+      2 -> "FAILURE",
+      130 -> "INTERRUPT",
+      131 -> "QUIT SIGNAL",
+      137 -> "KILL SIGNAL",
+      138 -> "BUS ERROR",
+      139 -> "SEGMENTATION VIOLATION",
+      143 -> "TERMINATION SIGNAL")
+
+  def print_return_code(rc: Int): String =
+  {
+    val text = return_code_text.get(rc)
+    "Return code: " + rc + (if (text.isEmpty) "" else " (" + text.get + ")")
+  }
+
   def print_rc(rc: Int): String = "return code " + rc
 }