Meta: Remove 'time' invocation in lint-ci

Some systems don't have /usr/bin/time available, and during most runs
of lint-ci we don't actually care that much about the exact timing.
Therefore, let's just remove it. It's easy enough to add back in, if
someone wants to investigate an issue.
This commit is contained in:
Ben Wiederhake 2022-09-20 15:03:36 +02:00 committed by Andreas Kling
parent edfef8e2f5
commit 48062b3cca
Notes: sideshowbarker 2024-07-17 06:44:16 +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 "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' | time xargs ./Build/lagom/Tools/IPCMagicLinter/IPCMagicLinter; then
if time { git ls-files '*.ipc' | 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)"