src/Pure/System/process_result.scala
changeset 77243 629dce95bb5c
parent 75393 87ebf5a50283
child 77253 792dad9cb04f
--- 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(