From 3dcd8f7f96dfdd910cd32f504f9e1fb25052484e Mon Sep 17 00:00:00 2001
From: degomme <augustin.degomme@unibas.ch>
Date: Wed, 6 Apr 2016 12:29:11 +0200
Subject: [PATCH] Switch to actually perform out-of-source builds. This should
 expose some issues. next step would be to rename the first "build" folder,
 but I want to see how this turns out first.

---
 tools/jenkins/build.sh | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/tools/jenkins/build.sh b/tools/jenkins/build.sh
index aa72529c2f..cda077ebdc 100755
--- a/tools/jenkins/build.sh
+++ b/tools/jenkins/build.sh
@@ -102,7 +102,9 @@ if test "$(uname -o)" != "Msys"; then
   echo "XX"
   tar xzf `cat VERSION`.tar.gz
   cd `cat VERSION`
-  SRCFOLDER="."
+  mkdir build
+  cd build
+  SRCFOLDER=".."
 else
 #for windows we don't make dist, but we still want to build out of source
   SRCFOLDER=$WORKSPACE
-- 
2.20.1