diff options
| author | Ben Wiederhake <BenWiederhake.GitHub@gmx.de> | 2022-09-20 15:03:36 +0200 |
|---|---|---|
| committer | Andreas Kling <kling@serenityos.org> | 2022-09-22 00:45:10 +0200 |
| commit | 48062b3cca05be9afd34137575c3880bfa7a5b2a (patch) | |
| tree | 5852736f74a2f16382a5ea250e04b109ff6613ad /Meta/lint-ci.sh | |
| parent | edfef8e2f5e27be597642c0d6310521b96ee237d (diff) | |
| download | serenity-48062b3cca05be9afd34137575c3880bfa7a5b2a.zip | |
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.
Diffstat (limited to 'Meta/lint-ci.sh')
| -rwxr-xr-x | Meta/lint-ci.sh | 4 |
1 files changed, 2 insertions, 2 deletions
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)" |