From 4763066f939ed491da13605b5c90f5e7b9d95d27 Mon Sep 17 00:00:00 2001
From: degomme <augustin.degomme@unibas.ch>
Date: Fri, 15 Jan 2016 16:22:32 +0100
Subject: [PATCH 1/1] oops

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

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