From c32afcc4038b1234219137cae196f3f776533d2f Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.oliveiramaroneze@cea.fr> Date: Thu, 28 May 2020 22:32:10 +0200 Subject: [PATCH] [analysis-scripts] add fallback when /usr/bin/time does not exist --- share/analysis-scripts/frama-c.mk | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/share/analysis-scripts/frama-c.mk b/share/analysis-scripts/frama-c.mk index db18e0999fe..b427e63aef0 100644 --- a/share/analysis-scripts/frama-c.mk +++ b/share/analysis-scripts/frama-c.mk @@ -74,14 +74,26 @@ endif UNAME := $(shell uname -s) ifeq ($(UNAME),Darwin) SED_UNBUFFERED:=sed +ifneq (,$(wildcard /usr/bin/time)) define time_with_output /usr/bin/time -p endef +else +define time_with_output + time +endef +endif else SED_UNBUFFERED:=sed --unbuffered +ifneq (,$(wildcard /usr/bin/time)) define time_with_output /usr/bin/time --format='user_time=%U\nmemory=%M' --output="$(1)" endef +else +define time_with_output + time +endef +endif endif # --- Utilities --- -- GitLab