# HG changeset patch # User wenzelm # Date 1601386701 -7200 # Node ID 4075560b3d5cc0aaf897ea1896653b6a22e93a9c # Parent 41a4352c52400405caa3fe5412dec68ef18117c8 clarified message; diff -r 41a4352c5240 -r 4075560b3d5c src/Pure/System/process_result.scala --- a/src/Pure/System/process_result.scala Tue Sep 29 15:30:47 2020 +0200 +++ b/src/Pure/System/process_result.scala Tue Sep 29 15:38:21 2020 +0200 @@ -20,6 +20,7 @@ Map(0 -> "OK", 1 -> "ERROR", 2 -> "FAILURE", + 127 -> "COMMAND NOT FOUND", 130 -> "INTERRUPT", 131 -> "QUIT SIGNAL", 137 -> "KILL SIGNAL",