From 48062b3cca05be9afd34137575c3880bfa7a5b2a Mon Sep 17 00:00:00 2001
From: Ben Wiederhake <BenWiederhake.GitHub@gmx.de>
Date: Tue, 20 Sep 2022 15:03:36 +0200
Subject: 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.
---
 Meta/lint-ci.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Meta')

diff --git a/Meta/lint-ci.sh b/Meta/lint-ci.sh
index 501dc20061..19784253c7 100755
--- a/Meta/lint-ci.sh
+++ b/Meta/lint-ci.sh
@@ -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)"
-- 
cgit v1.2.3