diff options
Diffstat (limited to 'build_tools.sh')
| -rwxr-xr-x | build_tools.sh | 6 |
1 files changed, 3 insertions, 3 deletions
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 |