From d1127622f5e4aa2abf6b492f6e43c0e17c3e0442 Mon Sep 17 00:00:00 2001 From: Jakub Narebski Date: Fri, 28 May 2010 21:11:23 +0200 Subject: [PATCH] git-instaweb: Remove pidfile after stopping web server 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 Acked-by: Petr Baudis Acked-by: Eric Wong Signed-off-by: Junio C Hamano --- git-instaweb.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/git-instaweb.sh b/git-instaweb.sh index 5c700b61a..a8c5dc0ee 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 -- 2.30.2