diff --git a/build_tools.sh b/build_tools.sh
index 675207b96..93f6065be 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