# HG changeset patch
# User wenzelm
# Date 1612729668 -3600
# Node ID da0ee7fbc06826a3af9dde61ae6d0afec3de4296
# Parent  4d36070bdbf49e6ebf8500e2a9abd19d93d252d7
terminate faster (following dd9fc8a3036c);

diff -r 4d36070bdbf4 -r da0ee7fbc068 src/Pure/System/bash.ML
--- a/src/Pure/System/bash.ML	Sun Feb 07 21:25:21 2021 +0100
+++ b/src/Pure/System/bash.ML	Sun Feb 07 21:27:48 2021 +0100
@@ -24,9 +24,9 @@
             (kill s; kill Kill.SIGNONE) andalso
             (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
         val _ =
-          multi_kill 10 Kill.SIGINT andalso
-          multi_kill 10 Kill.SIGTERM andalso
-          multi_kill 10 Kill.SIGKILL;
+          multi_kill 7 Kill.SIGINT andalso
+          multi_kill 3 Kill.SIGTERM andalso
+          multi_kill 1 Kill.SIGKILL;
       in () end;
 
 end;