2021-10-01 06:32:37 +00:00
|
|
|
#!/usr/bin/env bash
|
|
|
|
|
# Kill processes
|
|
|
|
|
|
2022-07-15 07:31:22 +00:00
|
|
|
set -Euo pipefail
|
2022-01-26 23:14:20 +00:00
|
|
|
|
2021-10-01 06:32:37 +00:00
|
|
|
# First parameter is the file with
|
|
|
|
|
# one pid per line.
|
|
|
|
|
if [ -f "$1" ]; then
|
|
|
|
|
while read pid
|
|
|
|
|
do
|
2022-01-31 22:55:06 +00:00
|
|
|
# handle the case of blank lines
|
|
|
|
|
[[ -n "$pid" ]] || continue
|
|
|
|
|
|
2021-10-01 06:32:37 +00:00
|
|
|
echo killing $pid
|
2022-12-02 14:20:43 +00:00
|
|
|
kill $pid || true
|
2021-10-01 06:32:37 +00:00
|
|
|
done < $1
|
|
|
|
|
fi
|
|
|
|
|
|
|
|
|
|
|
