diff -r 7c89e848bd18 -r 629dce95bb5c src/Pure/System/process_result.scala --- a/src/Pure/System/process_result.scala Sat Feb 11 14:24:20 2023 +0100 +++ b/src/Pure/System/process_result.scala Sat Feb 11 16:38:29 2023 +0100 @@ -13,6 +13,7 @@ val ok = 0 val error = 1 val failure = 2 + val startup_failure = 127 val interrupt = 130 val timeout = 142 @@ -38,6 +39,10 @@ def print_long(rc: Int): String = "Return code: " + rc + text(rc) def print(rc: Int): String = "return code " + rc + text(rc) } + + val ok: Process_Result = Process_Result(RC.ok) + val error: Process_Result = Process_Result(RC.error) + val startup_failure: Process_Result = Process_Result(RC.startup_failure) } final case class Process_Result(