diff options
-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 } |