diff --git a/run/server.sh b/run/server.sh index 1774a3f..6a7cbef 100644 --- a/run/server.sh +++ b/run/server.sh @@ -6,11 +6,13 @@ script_name=${BASH_SOURCE[0]} for pid in $(pidof -x $script_name); do if [ $pid != $$ ]; then - kill -9 $pid 2> /dev/null + kill -15 $pid 2> /dev/null wait $pid 2> /dev/null fi done +trap exit SIGINT SIGTERM + # Serve the page HTML="