2017-12-04 01:42:55 +00:00
|
|
|
#!/bin/sh
|
2019-08-15 20:17:13 +01:00
|
|
|
|
2019-08-27 14:15:44 +01:00
|
|
|
echo "This script is deprecated. Next time, run \"make tools\" instead."
|
2019-08-15 20:17:13 +01:00
|
|
|
for dname in tools/*; do
|
2019-08-27 14:15:44 +01:00
|
|
|
if [ -f ${dname}/Makefile ]; then
|
|
|
|
|
make -C ${dname} CXX=${1:-g++} --no-print-directory
|
2019-08-15 20:17:13 +01:00
|
|
|
fi
|
|
|
|
|
done
|
