# HG changeset patch
# User wenzelm
# Date 1457456111 -3600
# Node ID c46418f12ee149e582ecacc3794b7ea18f80e86f
# Parent  a4ea3a222e0ed17ce023e2a07583ef6197747174
clarified process interrupt: exactly one signal (like thread interrupt);

diff -r a4ea3a222e0e -r c46418f12ee1 src/Pure/Concurrent/bash.scala
--- a/src/Pure/Concurrent/bash.scala	Tue Mar 08 17:52:33 2016 +0100
+++ b/src/Pure/Concurrent/bash.scala	Tue Mar 08 17:55:11 2016 +0100
@@ -59,6 +59,9 @@
 
     private val pid = stdout.readLine
 
+    def interrupt()
+    { Exn.Interrupt.postpone { Isabelle_System.kill("INT", pid) } }
+
     private def kill(signal: String): Boolean =
       Exn.Interrupt.postpone {
         Isabelle_System.kill(signal, pid)
@@ -80,7 +83,6 @@
       running
     }
 
-    def interrupt() { multi_kill("INT") }
     def terminate() { multi_kill("INT") && multi_kill("TERM") && kill("KILL"); proc.destroy }