Fixed bugs preventing correct path detection.
This commit is contained in:
parent
362ee08272
commit
2520701f37
1 changed files with 3 additions and 2 deletions
|
@ -20,7 +20,7 @@ enable_papi=${enable_papi:=1}
|
||||||
|
|
||||||
# MAKEOPTS="-j1"
|
# MAKEOPTS="-j1"
|
||||||
|
|
||||||
[[ -z "${MPI_DIR// }" ]] || sit_fail "Installation requires MPI. No MPI installation found."
|
[[ -z "$MPI_DIR" ]] && sit_fail "Installation requires MPI. No MPI installation found."
|
||||||
|
|
||||||
|
|
||||||
# Other interesting configure options:
|
# Other interesting configure options:
|
||||||
|
@ -43,7 +43,8 @@ esac
|
||||||
# use PAPI
|
# use PAPI
|
||||||
if [ $enable_papi != 0 ] ; then
|
if [ $enable_papi != 0 ] ; then
|
||||||
PAPI_DIR=$(dirname $(dirname $(which papi_avail)))
|
PAPI_DIR=$(dirname $(dirname $(which papi_avail)))
|
||||||
[ -z "${PAPI_DIR// }" ] || sit_fail "PAPI diretory not found!"
|
[ -z "${PAPI_DIR/\//}" ] && sit_fail "PAPI diretory not found!"
|
||||||
|
sit_info "PAPI_DIR: $PAPI_DIR"
|
||||||
CONFIGURE_OPTS="$CONFIGURE_OPTS --with-papi=$PAPI_DIR"
|
CONFIGURE_OPTS="$CONFIGURE_OPTS --with-papi=$PAPI_DIR"
|
||||||
else
|
else
|
||||||
CONFIGURE_OPTS="$CONFIGURE_OPTS --without-papi"
|
CONFIGURE_OPTS="$CONFIGURE_OPTS --without-papi"
|
||||||
|
|
Loading…
Reference in a new issue