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 <redacted>
Acked-by: Petr Baudis <redacted>
Acked-by: Eric Wong <redacted>
Signed-off-by: Junio C Hamano <redacted>

diff --git a/git-instaweb.sh b/git-instaweb.sh
index 5c700b61a8998f6bb35017f50d79bd18de57ec46..a8c5dc0ee2202606176caae38fdcbb297296cabd 100755 (executable)
--- 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