src/Pure/System/bash.scala
changeset 73858 37243ad3ecb6
parent 73857 19c558ea903c
child 73859 342362c9496c
--- a/src/Pure/System/bash.scala	Thu Apr 22 23:03:58 2021 +0200
+++ b/src/Pure/System/bash.scala	Thu Apr 22 23:40:22 2021 +0200
@@ -11,6 +11,7 @@
   BufferedWriter, OutputStreamWriter}
 
 import scala.annotation.tailrec
+import scala.jdk.OptionConverters._
 
 
 object Bash
@@ -91,12 +92,18 @@
 
     private val group_pid = stdout.readLine
 
+    private val initial_process: Option[ProcessHandle] =
+      if (Platform.is_unix) ProcessHandle.of(Value.Long.parse(group_pid)).toScala
+      else None
+
     @tailrec private def signal(s: String, count: Int = 1): Boolean =
     {
       count <= 0 ||
       {
         Isabelle_System.process_signal(group_pid, signal = s)
-        val running = Isabelle_System.process_signal(group_pid)
+        val running =
+          (initial_process.isDefined && initial_process.get.isAlive) ||
+          Isabelle_System.process_signal(group_pid)
         if (running) {
           Time.seconds(0.1).sleep
           signal(s, count - 1)