diff --git a/share/analysis-scripts/frama-c.mk b/share/analysis-scripts/frama-c.mk index db18e0999fe2219969fc0f5e3ea63180f45e9955..b427e63aef0dcf4fe43462cc1ce061c469d05b1a 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 ---