From ec24b5df3c190e8cbb1d64cfdf5ccc04457b9bc5 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 23 Aug 2021 16:26:40 +0200
Subject: [PATCH] [analysis-scripts] simplify checking of 'time' command
 options

---
 share/analysis-scripts/analysis.mk | 25 ++++++-------------------
 1 file changed, 6 insertions(+), 19 deletions(-)

diff --git a/share/analysis-scripts/analysis.mk b/share/analysis-scripts/analysis.mk
index 2c97f34cc84..9cfd6d29109 100644
--- a/share/analysis-scripts/analysis.mk
+++ b/share/analysis-scripts/analysis.mk
@@ -69,32 +69,19 @@ endif
 # nor Busybox' have it, in which case we ignore it)
 SED_UNBUFFERED:=sed$(shell sed --unbuffered //p /dev/null 2>/dev/null && echo " --unbuffered" || true)
 
-# Test if on a Mac;
-# test if /usr/bin/time is available, otherwise use the shell builtin
-# (which has less options)
-UNAME := $(shell uname -s)
-ifeq ($(UNAME),Darwin)
-ifneq (,$(wildcard /usr/bin/time))
+# 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 $$?))
 define time_with_output
-  /usr/bin/time -p
+  $(shell which time) -f 'user_time=%U\nmemory=%M' -o "$(1)"
 endef
 else
 define time_with_output
   time
 endef
 endif
-else
-TIMEBIN:=$(shell which -a time | grep '^/')
-ifneq (,$(TIMEBIN))
-define time_with_output
-  $(TIMEBIN) -f 'user_time=%U\nmemory=%M' -o "$(1)"
-endef
-else
-define time_with_output
-  time
-endef
-endif
-endif
 
 # --- Utilities ---
 
-- 
GitLab