author | wenzelm |
Sun, 07 Feb 2021 21:27:48 +0100 | |
changeset 73234 | da0ee7fbc068 |
parent 73233 | 4d36070bdbf4 |
child 73235 | 4e631963fe24 |
--- 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;