Skip to content

kill_server.sh: Avoid non-standard --timeout option for kill command

Thomas Ives requested to merge fix-kill-servers into main

On some systems, kill does not support the --timeout option, making this script not portable. We replace the --timeout usage with a more portable implementation of the same behaviour in bash.

Closes #1127 (closed).

Merge request reports