# 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;