src/Pure/System/bash.scala
changeset 74306 a117c076aa22
parent 74273 0a4cdf0036a0
child 75393 87ebf5a50283
--- 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)
     }