diff --git a/tools/jenkins/run_jenkins.sh b/tools/jenkins/run_jenkins.sh
index 57cec774248..5e8ddb92fcf 100755
--- a/tools/jenkins/run_jenkins.sh
+++ b/tools/jenkins/run_jenkins.sh
@@ -68,6 +68,7 @@ then
   else
     echo "Docker exited with failure, keeping container $DOCKER_CID."
     echo "You can SSH to the worker and use 'docker start CID' and 'docker exec -i -t CID bash' to debug the problem."
+    exit 1
   fi
 
 elif [ "$platform" == "windows" ]