diff options
author | Jakub Narebski <jnareb@gmail.com> | 2010-05-28 21:11:23 +0200 |
---|---|---|
committer | Junio C Hamano <gitster@pobox.com> | 2010-06-02 11:49:24 -0700 |
commit | d1127622f5e4aa2abf6b492f6e43c0e17c3e0442 (patch) | |
tree | 6219f2939b27b665557def5b7bdf15823aff8587 /git-instaweb.sh | |
parent | c0cb4ed3e653a37a53ef3a1e08daa42ac9cbc3fc (diff) | |
download | git-d1127622f5e4aa2abf6b492f6e43c0e17c3e0442.tar.gz |
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 <jnareb@gmail.com>
Acked-by: Petr Baudis <pasky@suse.cz>
Acked-by: Eric Wong <normalperson@yhbt.net>
Signed-off-by: Junio C Hamano <gitster@pobox.com>
Diffstat (limited to 'git-instaweb.sh')
-rwxr-xr-x | git-instaweb.sh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/git-instaweb.sh b/git-instaweb.sh index 5c700b61a8..a8c5dc0ee2 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 |