From ecf5149e979887ca7d34ec818fd6e57ad5f37d94 Mon Sep 17 00:00:00 2001
From: Pietro Incardona <incardon@mpi-cbg.de>
Date: Mon, 24 Jul 2017 13:41:43 +0200
Subject: [PATCH] Fixing window10 branch name

---
 build_sec_OS.sh | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/build_sec_OS.sh b/build_sec_OS.sh
index 98d883096..652996935 100755
--- a/build_sec_OS.sh
+++ b/build_sec_OS.sh
@@ -4,6 +4,7 @@
 
 echo "Directory: $1"
 echo "Machine: $2"
+echo "Branch: $BRANCH_NAME"
 
 mkdir src/config
 
@@ -12,13 +13,11 @@ if [ "$2" == "windows10" ]; then
     echo "Compiling on windows10"
 
     echo "1" > input_install
-    echo "1" >> input_install
-    echo "1" >> input_install
     echo "2" >> input_install
     echo "y" >> input_install
     echo "1" >> input_install
 
-    ./install -i "/scratch/p_ppm/openfpm_deps_intel" < input_install
+    ./install -i "/home/jenkins/$BRANCH_NAME" < input_install
 
 fi
 
-- 
GitLab