# 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",