diff --git a/tools/build-utils.sh b/tools/build-utils.sh index 1874c901b77e9d2f8438b79c3d15a17f30d1f81c..7fd07886fa63bbfb51b3c9354a179b1004346095 100755 --- a/tools/build-utils.sh +++ b/tools/build-utils.sh @@ -42,7 +42,15 @@ EOF if [ "$MAKE" = "" ] then MAKE="`which gmake`" - if echo $MAKE | grep '^no' > /dev/null; then + + # Some versions of which set an error code if it fails. Others + # say "no foo in <path>". In either of these cases, just assume + # make is GNU make. + + if [ $? -ne 0 ]; then + MAKE="make" + fi + if echo "X$MAKE" | grep '^Xno' > /dev/null; then MAKE="make" fi fi