From 673dd7d1507e505024a8ca0ac0179183bd8ccd7d Mon Sep 17 00:00:00 2001
From: Gabriel Corona <gabriel.corona@loria.fr>
Date: Mon, 27 Jul 2015 15:23:05 +0200
Subject: [PATCH] [jenkins] ulimit -c may not be available

---
 buildtools/jenkins/build.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/buildtools/jenkins/build.sh b/buildtools/jenkins/build.sh
index cea66c31a8..9789271a25 100755
--- a/buildtools/jenkins/build.sh
+++ b/buildtools/jenkins/build.sh
@@ -34,7 +34,7 @@ onoff() {
   fi
 }
 
-ulimit -c 0
+ulimit -c 0 || true
 
 if [ -d $WORKSPACE/build ]
 then
-- 
2.20.1