From 1a6c8a4e6716921d901e926bb01a573bde14df46 Mon Sep 17 00:00:00 2001
From: Peter Simonyi <peter@steamedpears.com>
Date: Tue, 16 Apr 2013 21:21:02 -0400
Subject: [PATCH] Kill the servers with SIGTERM to let them clean up

Redis, in particular, needs to write the database to disk.
---
 bin/stop_dev.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/bin/stop_dev.sh b/bin/stop_dev.sh
index 6a42390..f42ab89 100755
--- 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)