tools/configure.sh: Fix last commit. If gmake is not present, then 'which gmake' spews a lot of annoying error messages when configuring. Best to pipe stderr to /dev/null so that we are blessedly unaware of the failures.
This commit is contained in:
parent
f6e087a05c
commit
31e3f208b2
|
@ -1,7 +1,8 @@
|
||||||
#!/bin/bash
|
#!/bin/bash
|
||||||
# configure.sh
|
# configure.sh
|
||||||
#
|
#
|
||||||
# Copyright (C) 2007, 2008, 2011, 2015, 2017 Gregory Nutt. All rights reserved.
|
# Copyright (C) 2007, 2008, 2011, 2015, 2017-2018 Gregory Nutt. All rights
|
||||||
|
# reserved.
|
||||||
# Author: Gregory Nutt <gnutt@nuttx.org>
|
# Author: Gregory Nutt <gnutt@nuttx.org>
|
||||||
#
|
#
|
||||||
# Redistribution and use in source and binary forms, with or without
|
# Redistribution and use in source and binary forms, with or without
|
||||||
|
@ -325,8 +326,9 @@ fi
|
||||||
|
|
||||||
echo " Refreshing..."
|
echo " Refreshing..."
|
||||||
cd ${TOPDIR} || { echo "Failed to cd to ${TOPDIR}"; exit 1; }
|
cd ${TOPDIR} || { echo "Failed to cd to ${TOPDIR}"; exit 1; }
|
||||||
|
|
||||||
MAKE_BIN=make
|
MAKE_BIN=make
|
||||||
if [ ! -z `which gmake` ]; then
|
if [ ! -z `which gmake 2>/dev/null` ]; then
|
||||||
MAKE_BIN=gmake
|
MAKE_BIN=gmake
|
||||||
fi
|
fi
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue