diff options
| author | PikalaxALT <pikalaxalt@gmail.com> | 2019-08-27 09:15:44 -0400 |
|---|---|---|
| committer | PikalaxALT <pikalaxalt@gmail.com> | 2019-08-27 09:15:44 -0400 |
| commit | 40c1db11067a152865db10f2f5399354a4268c91 (patch) | |
| tree | fe0f74e2ea6d701d959009d0449a8a9e7304e1fb | |
| parent | 4541b959b624e8298e9791d69dfac5630cd6a122 (diff) | |
Update deprecated build_tools script
| -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 |