From a51c1f3d46af1ec1d93fb3431f1d783ee098705a Mon Sep 17 00:00:00 2001 From: samuel Date: Sun, 7 May 2023 15:34:50 +0200 Subject: [PATCH] [Fix] Correct mistake in kill command --- src/deployer.sh | 2 +- src/runner.sh | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/deployer.sh b/src/deployer.sh index dd1a2ff..7be219b 100755 --- a/src/deployer.sh +++ b/src/deployer.sh @@ -440,7 +440,7 @@ main() ( fail "Deployer process with pid='${pid}' is not running." \ "${err_deployer_process_not_running}" fi - if ! kill "${pid}" || kill --signal KILL "${pid}"; then + if ! kill "${pid}" || kill -KILL "${pid}"; then fail "Cannot kill deployer process." \ "${err_deployer_process_not_killed}" fi diff --git a/src/runner.sh b/src/runner.sh index d78451e..0a03805 100755 --- a/src/runner.sh +++ b/src/runner.sh @@ -541,7 +541,7 @@ main() ( fail "Runner process with pid='${pid}' is not running." \ "${err_runner_process_not_running}" fi - if ! kill "${pid}" || kill --signal KILL "${pid}"; then + if ! kill "${pid}" || kill -KILL "${pid}"; then fail "Cannot kill runner process." "${err_runner_process_not_killed}" fi rm --force "${runner_sock}"