terminate faster (following dd9fc8a3036c);
authorwenzelm
Sun, 07 Feb 2021 21:27:48 +0100
changeset 73234 da0ee7fbc068
parent 73233 4d36070bdbf4
child 73235 4e631963fe24
terminate faster (following dd9fc8a3036c);
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;