Meta: Use time instead of /usr/bin/time in lint-ci.sh

I totally overlooked that /usr/bin/time is not universal, which broke
some systems. This commit instead calls 'time', allowing either a shell
built-in to kick in, or a (potentially different) binary be found
anywhere in the PATH.
This commit is contained in:
Ben Wiederhake 2022-09-19 19:45:04 +02:00 committed by Ali Mohammad Pur
parent ef507720f0
commit 230226028a
Notes: sideshowbarker 2024-07-17 17:49:11 +09:00

View file

@ -34,7 +34,7 @@ for cmd in \
Meta/lint-python.sh \
Meta/lint-shell-scripts.sh; do
echo "Running ${cmd}"
if "/usr/bin/time" "${cmd}" "$@"; then
if "time" "${cmd}" "$@"; then
echo -e "[${GREEN}OK${NC}]: ${cmd}"
else
echo -e "[${RED}FAIL${NC}]: ${cmd}"
@ -44,7 +44,7 @@ done
if [ -x ./Build/lagom/Tools/IPCMagicLinter/IPCMagicLinter ]; then
echo "Running IPCMagicLinter"
if git ls-files '*.ipc' | /usr/bin/time xargs ./Build/lagom/Tools/IPCMagicLinter/IPCMagicLinter; then
if git ls-files '*.ipc' | time xargs ./Build/lagom/Tools/IPCMagicLinter/IPCMagicLinter; then
echo -e "[${GREEN}OK${NC}]: IPCMagicLinter (in Meta/lint-ci.sh)"
else
echo -e "[${RED}FAIL${NC}]: IPCMagicLinter (in Meta/lint-ci.sh)"
@ -55,7 +55,7 @@ else
fi
echo "Running Meta/lint-clang-format.sh"
if /usr/bin/time Meta/lint-clang-format.sh --overwrite-inplace "$@" && git diff --exit-code; then
if time Meta/lint-clang-format.sh --overwrite-inplace "$@" && git diff --exit-code; then
echo -e "[${GREEN}OK${NC}]: Meta/lint-clang-format.sh"
else
echo -e "[${RED}FAIL${NC}]: Meta/lint-clang-format.sh"
@ -70,7 +70,7 @@ fi
#
if [ "$ports" = true ]; then
echo "Running Meta/lint-ports.py"
if /usr/bin/time Meta/lint-ports.py; then
if time Meta/lint-ports.py; then
echo -e "[${GREEN}OK${NC}]: Meta/lint-ports.py"
else
echo -e "[${RED}FAIL${NC}]: Meta/lint-ports.py"