diff --git a/build.sh b/build.sh index 35ce0831665ce378900fc5cf02b038b86d38fa24..c329a81ee460c999425b42c75c4748a4711638a1 100644 --- a/build.sh +++ b/build.sh @@ -18,15 +18,17 @@ fi if [ "$xInSource" = "InSource+" ] ; then CONFIGURE="./configure" else - MUSIC_VPATH=$WORKSPACE/build + MUSIC_VPATH=build mkdir "$MUSIC_VPATH" cd "$MUSIC_VPATH" CONFIGURE="../configure" fi -MUSIC_RESULT=$WORKSPACE/result +MUSIC_RESULT=result mkdir "$MUSIC_RESULT" +MUSIC_RESULT=$(readlink -f $MUSIC_RESULT) + $CONFIGURE \ --prefix="$MUSIC_RESULT" \ $CONFIGURE_MPI