From 2366f6af8641c11966d355beddf83e89dbf5c459 Mon Sep 17 00:00:00 2001
From: "Nicolas \"Pixel\" Noble" <pixel@nobis-crew.org>
Date: Sat, 11 Jul 2015 01:26:32 +0200
Subject: [PATCH] Let's workaround #2140 a bit.

Let's wait 4 seconds before removing the docker container, and let's make the removal a non-fatal condition of the jenkins script.
---
 tools/jenkins/run_jenkins.sh | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/tools/jenkins/run_jenkins.sh b/tools/jenkins/run_jenkins.sh
index 16eb6bea6e5..af49ea0bd03 100755
--- 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