changeset 1548:61c03265e133

launching script: use SIGTERM instead of SIGINT with the “stop” command
author Goffi <goffi@goffi.org>
date Mon, 02 Nov 2015 22:02:41 +0100
parents 0632d96f08ad
children e987325c14ef
files src/sat.sh
diffstat 1 files changed, 1 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/sat.sh	Mon Nov 02 22:02:41 2015 +0100
+++ b/src/sat.sh	Mon Nov 02 22:02:41 2015 +0100
@@ -10,7 +10,7 @@
         PID=`cat $1`
         if ps -p $PID > /dev/null; then
             echo "Terminating $2... "
-            kill -INT $PID
+            kill $PID
         else
             echo "No running process of ID $PID... removing PID file"
             rm -f $1