From 31e3f208b256a454249fedc190e28c4ae2d9e0b3 Mon Sep 17 00:00:00 2001
From: Gregory Nutt <gnutt@nuttx.org>
Date: Wed, 25 Apr 2018 08:28:49 -0600
Subject: [PATCH] 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.

---
 tools/configure.sh | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/tools/configure.sh b/tools/configure.sh
index 78a6c7b830..d8266b1c18 100755
--- a/tools/configure.sh
+++ b/tools/configure.sh
@@ -1,7 +1,8 @@
 #!/bin/bash
 # 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>
 #
 # Redistribution and use in source and binary forms, with or without
@@ -325,8 +326,9 @@ fi
 
 echo "  Refreshing..."
 cd ${TOPDIR} || { echo "Failed to cd to ${TOPDIR}"; exit 1; }
+
 MAKE_BIN=make
-if [ ! -z `which gmake` ]; then
+if [ ! -z `which gmake 2>/dev/null` ]; then
   MAKE_BIN=gmake
 fi