From 0a8a5624df736b7d450da922a37562729df10847 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 23 Aug 2021 16:31:25 +0200
Subject: [PATCH] [scripts] more portable detection of 'time' command, take 2

---
 share/analysis-scripts/analysis.mk | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/share/analysis-scripts/analysis.mk b/share/analysis-scripts/analysis.mk
index 9cfd6d29109..4e545c9e747 100644
--- a/share/analysis-scripts/analysis.mk
+++ b/share/analysis-scripts/analysis.mk
@@ -70,12 +70,12 @@ endif
 SED_UNBUFFERED:=sed$(shell sed --unbuffered //p /dev/null 2>/dev/null && echo " --unbuffered" || true)
 
 # If there is a GNU time in the PATH, which contains the desired options
-# (-f and -o, whose presence is tested using the --help message),
-# use them; otherwise, use any time (be it a shell builtin or a command).
-# Note: usage of 'env' is necessary to avoid invoking a shell builtin.
-ifneq (1,$(shell env time --help | grep -C100 '\-f' | grep '\-o' -q; echo $$?))
+# (-f and -o), use them; otherwise, use any time (be it a shell builtin
+# or a command). 'env' allows bypassing shell builtins (if they exist),
+# since they usually don't have the required options.
+ifeq (OK,$(shell env time -f 'test' -o '/dev/null' echo OK || echo KO))
 define time_with_output
-  $(shell which time) -f 'user_time=%U\nmemory=%M' -o "$(1)"
+  env time -f 'user_time=%U\nmemory=%M' -o "$(1)"
 endef
 else
 define time_with_output
-- 
GitLab