Merge pull request #2387 from nicolasnoble/docker-is-a-freezer

Let's workaround #2140 a bit.
10 years ago · 4547d503d3
parent 5421cab8f2 2366f6af86
commit 4547d503d3
1 changed files with 2 additions and 1 deletions
--- a/tools/jenkins/run_jenkins.sh
+++ b/tools/jenkins/run_jenkins.sh
@ -70,7 +70,8 @@ then
  DOCKER_CID=`cat docker.cid`
  docker kill $DOCKER_CID
  docker cp $DOCKER_CID:/var/local/git/grpc/report.xml $git_root
-  docker rm $DOCKER_CID
+  sleep 4
+  docker rm $DOCKER_CID || true

 elif [ "$platform" == "windows" ]
 then