src/Pure/System/bash.ML
changeset 73234 da0ee7fbc068
parent 73230 d1bc5a376cf9
child 73244 5bded25065f8
--- 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;