diff options
-rw-r--r-- | configure.pl | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/configure.pl b/configure.pl index 6357520..d2bc962 100644 --- a/configure.pl +++ b/configure.pl @@ -49,7 +49,7 @@ if("$ENV{MPI_DIR}" =~ /^\s*$/) { message("MPI selected, but MPI_DIR is not set. Computing settings..."); $mpi_build = 1; $mpi_search = 1; -} elsif(-d $ENV{MPI_DIR}) { +} elsif(-d $ENV{MPI_DIR} or $ENV{MPI_DIR} eq "NO_BUILD") { $mpi_dir = $ENV{MPI_DIR}; $mpi_search = 0; $mpi_build = 0; @@ -57,9 +57,6 @@ if("$ENV{MPI_DIR}" =~ /^\s*$/) { } elsif($ENV{MPI_DIR} eq "BUILD") { $mpi_build = 1; $mpi_search = 0; -} elsif($ENV{MPI_DIR} eq "NO_BUILD") { - $mpi_build = 0; - $mpi_search = 0; } else { $mpi_build = 1; $mpi_search = 1; |