From: Jakub Narebski Date: Fri, 28 May 2010 19:11:23 GMT Subject: [PATCH 1/3] git-instaweb: Remove pidfile after stopping web server Message-ID: <1275073885-26537-2-git-send-email-jnareb@gmail.com> In-Reply-To: <1275073885-26537-1-git-send-email-jnareb@gmail.com> This way running e.g. "git instaweb" after "git instaweb --stop" would not try to kill already stopped web server. This is probably important only for those web servers that are "daemonized" by git-instaweb itself, i.e. for those where it is git-instaweb that creates pidfile. Currently it is includes only 'mongoose' web server, but it would also include 'plackup' web server (added in later commit). Signed-off-by: Jakub Narebski --- git-instaweb.sh | 1 + 1 files changed, 1 insertions(+), 0 deletions(-) diff --git a/git-instaweb.sh b/git-instaweb.sh index 5c700b6..a8c5dc0 100755 --- a/git-instaweb.sh +++ b/git-instaweb.sh @@ -114,6 +114,7 @@ EOF stop_httpd () { test -f "$fqgitdir/pid" && kill $(cat "$fqgitdir/pid") + rm -f "$fqgitdir/pid" } while test $# != 0 -- 1.7.0.1