--- a/src/Pure/System/bash.scala Sun Sep 12 22:31:51 2021 +0200
+++ b/src/Pure/System/bash.scala Mon Sep 13 11:52:32 2021 +0200
@@ -230,7 +230,7 @@
val rc =
try { join() }
- catch { case Exn.Interrupt() => terminate(); Process_Result.interrupt_rc }
+ catch { case Exn.Interrupt() => terminate(); Process_Result.RC.interrupt }
watchdog_thread.foreach(_.cancel())
@@ -238,7 +238,7 @@
out_lines.join
err_lines.join
- if (strict && rc == Process_Result.interrupt_rc) throw Exn.Interrupt()
+ if (strict && rc == Process_Result.RC.interrupt) throw Exn.Interrupt()
Process_Result(rc, out_lines.join, err_lines.join, get_timing)
}