diff --git a/script/server b/script/server index 8e1b5b00..ebace09b 100755 --- a/script/server +++ b/script/server @@ -1,5 +1,13 @@ #!/bin/bash +reap() { + kill -TERM $child + sleep 0.1 + exit +} + +trap reap TERM INT + # If a command fails, exit the script set -e