Merge pull request #157 from psimonyi/signals

Kill the servers with SIGTERM to let them clean up
SteamedPears · Apr 17, 2013 · 91cb41b · 91cb41b
2 parents c380807 + 1a6c8a4
commit 91cb41b
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/bin/stop_dev.sh b/bin/stop_dev.sh
@@ -18,5 +18,5 @@ DB_PID="var/db.pid"
 ######################################################################
 # Stop server and db
 
-kill -SIGKILL $(< $SERVER_PID)
-kill -SIGKILL $(< $DB_PID)
+kill -SIGTERM $(< $SERVER_PID)
+kill -SIGTERM $(< $DB_PID)