diff options
| author |  Craig Tiller <ctiller@google.com> | 2015-08-25 09:49:02 -0700 |
|---|---|---|
| committer | Craig Tiller <ctiller@google.com> | 2015-08-25 09:49:02 -0700 |
| commit | 3d20b000b7195bfdba1e472a7ca3f4bb366d3e75 (patch) | |
| tree | 5454653cd55c905762a7f3db9ffc7162cfcd3ddf /tools | |
| parent | 43fef09aecaa81a9e16e2b7ecc5598c223051f15 (diff) | |
Add a comment describing out views on killing
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/jenkins/run_jenkins.sh | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tools/jenkins/run_jenkins.sh b/tools/jenkins/run_jenkins.sh index 7bae48dc19..0f15835ea8 100755 --- a/tools/jenkins/run_jenkins.sh +++ b/tools/jenkins/run_jenkins.sh @@ -89,6 +89,9 @@ then bash -l /var/local/jenkins/grpc/tools/jenkins/docker_run_jenkins.sh || DOCKER_FAILED="true" DOCKER_CID=`cat docker.cid` + # forcefully kill the instance if it's still running, otherwise + # continue + # (failure to kill something that's already dead => things are dead) docker kill $DOCKER_CID || true docker cp $DOCKER_CID:/var/local/git/grpc/report.xml $git_root # TODO(ctiller): why? |