diff options
| author |  Shanqing Cai <cais@google.com> | 2017-06-06 12:18:03 -0400 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2017-06-06 12:18:03 -0400 |
| commit | 2be64b38e49ada5161b027bc08b558073d219351 (patch) | |
| tree | 5eb62e7357635d33a2a0ea98b3b3fd2db7d83689 /configure | |
| parent | aa2941ffd7c6b6ae10fcb476ac1b3190b115bfbb (diff) | |
| parent | edf3d5dbe405930e863c3b747e8a241e73903616 (diff) | |
Merge pull request #10417 from darrengarvey/fix-configure-enabling-mpi
configure: Fix default path when enabling MPI.
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -802,11 +802,11 @@ while true; do fromuser="" if [ -z "$MPI_HOME" ]; then #Get the base folder by removing the bin path - default_path=$(dirname $(dirname $(which mpirun)) || dirname $(dirname $(which mpiexec)) || true) + default_mpi_path=$(dirname $(dirname $(which mpirun)) || dirname $(dirname $(which mpiexec)) || true) read -p "Please specify the MPI toolkit folder. [Default is $default_mpi_path]: " MPI_HOME fromuser="1" if [ -z "$MPI_HOME" ]; then - MPI_HOME=$default_path + MPI_HOME=$default_mpi_path fi fi |