Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Switch to actually perform out-of-source builds.
authordegomme <augustin.degomme@unibas.ch>
Wed, 6 Apr 2016 10:29:11 +0000 (12:29 +0200)
committerdegomme <augustin.degomme@unibas.ch>
Wed, 6 Apr 2016 10:29:11 +0000 (12:29 +0200)
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

index aa72529..cda077e 100755 (executable)
@@ -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