# HG changeset patch
# User Goffi <goffi@goffi.org>
# Date 1446498161 -3600
# Node ID 61c03265e133369e8214049a2028b867d9b0dad7
# Parent  0632d96f08ad839bc60716d50a11a5cda53c6722
launching script: use SIGTERM instead of SIGINT with the “stop” command

diff -r 0632d96f08ad -r 61c03265e133 src/sat.sh
--- 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