From 40c1db11067a152865db10f2f5399354a4268c91 Mon Sep 17 00:00:00 2001
From: PikalaxALT <pikalaxalt@gmail.com>
Date: Tue, 27 Aug 2019 09:15:44 -0400
Subject: [PATCH] Update deprecated build_tools script

---
 build_tools.sh | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/build_tools.sh b/build_tools.sh
index 675207b966..93f6065be4 100755
--- a/build_tools.sh
+++ b/build_tools.sh
@@ -1,8 +1,8 @@
 #!/bin/sh
 
-echo "This script is deprecated. Run \"make tools\" instead."
+echo "This script is deprecated. Next time, run \"make tools\" instead."
 for dname in tools/*; do
-  if [[ -f ${dname}/Makefile ]]; then
-    make -C ${dname} CXX=${1:-g++}
+  if [ -f ${dname}/Makefile ]; then
+    make -C ${dname} CXX=${1:-g++} --no-print-directory
   fi
 done