diff options
| author | Chris Wilson <chris+github@qwirx.com> | 2008-12-16 17:37:08 +0000 |
|---|---|---|
| committer | Chris Wilson <chris+github@qwirx.com> | 2008-12-16 17:37:08 +0000 |
| commit | cd8ba14ab223ec91fc05045877fccaf818824d97 (patch) | |
| tree | 2c8274fb22130edea55952215903865d89a45096 | |
| parent | 3077653386796225506c06c0d9db430903666309 (diff) | |
Fix process kill function, fixes [2402] [2404].
Delete stale PID files after killing processes on Windows, as that
fine OS doesn't give them a chance to clean up for themselves.
| -rwxr-xr-x | infrastructure/makebuildenv.pl.in | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/infrastructure/makebuildenv.pl.in b/infrastructure/makebuildenv.pl.in index edd96063..8b91b972 100755 --- a/infrastructure/makebuildenv.pl.in +++ b/infrastructure/makebuildenv.pl.in @@ -405,9 +405,11 @@ for my $mod (@implicit_deps, @modules) print TESTFILE <<__E; kill_process() { - test -r testfiles/$1.pid \\ - && /bin/kill -0 -f `cat testfiles/$1.pid` \\ - && /bin/kill -f `cat testfiles/$1.pid` + if test -r testfiles/\$1.pid; then + /bin/kill -0 -f `cat testfiles/\$1.pid` \\ + && /bin/kill -f `cat testfiles/\$1.pid` + rm testfiles/\$1.pid + fi } __E } @@ -416,9 +418,9 @@ __E print TESTFILE <<__E; kill_process() { - test -r testfiles/$1.pid \\ - && kill -0 `cat testfiles/$1.pid` \\ - && kill `cat testfiles/$1.pid` + test -r testfiles/\$1.pid \\ + && kill -0 `cat testfiles/\$1.pid` \\ + && kill `cat testfiles/\$1.pid` } __E } |