diff --git a/share/analysis-scripts/analysis.mk b/share/analysis-scripts/analysis.mk index 0e4910e1acfeb82f018a68576adfdc200fdaa988..1705e9260f0285ecd6a8d71a5d7f6370250dbaff 100644 --- a/share/analysis-scripts/analysis.mk +++ b/share/analysis-scripts/analysis.mk @@ -84,7 +84,7 @@ 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)" + /usr/bin/time -f 'user_time=%U\nmemory=%M' -o "$(1)" endef else define time_with_output