diff options
Diffstat (limited to 'tools/jenkins')
| -rwxr-xr-x | tools/jenkins/run_jenkins.sh | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/tools/jenkins/run_jenkins.sh b/tools/jenkins/run_jenkins.sh index 6042655a27..f2091e2423 100755 --- a/tools/jenkins/run_jenkins.sh +++ b/tools/jenkins/run_jenkins.sh @@ -73,15 +73,7 @@ then DOCKER_CID=`cat docker.cid` docker kill $DOCKER_CID docker cp $DOCKER_CID:/var/local/git/grpc/report.xml $git_root - if [ "$DOCKER_FAILED" == "" ] - then - echo "Docker finished successfully, deleting the container $DOCKER_CID" - docker rm $DOCKER_CID - else - echo "Docker exited with failure, keeping container $DOCKER_CID." - echo "You can SSH to the worker and use 'docker commit CID YOUR_IMAGE_NAME' and 'docker run -i -t YOUR_IMAGE_NAME bash' to debug the problem." - exit 1 - fi + docker rm $DOCKER_CID elif [ "$platform" == "windows" ] then |