From 6a40259c3e510495e5cc226b571e33d2aad41e7a Mon Sep 17 00:00:00 2001
From: Jan Lindemann <jan@janware.com>
Date: Wed, 27 Dec 2017 12:59:55 +0000
Subject: [PATCH] defs.mk, timed-make-shell.sh: Beautify make benchmark

Signed-off-by: Jan Lindemann <jan@janware.com>
---
 make/defs.mk                | 8 ++++----
 scripts/timed-make-shell.sh | 3 +--
 2 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/make/defs.mk b/make/defs.mk
index 65d12b36..eddfe6a7 100644
--- a/make/defs.mk
+++ b/make/defs.mk
@@ -5,15 +5,15 @@
 ifndef JW_BUILD_DEF_MK_INCLUDED
 JW_BUILD_DEF_MK_INCLUDED = true
 
+ifeq ($(MAKE_BENCHMARK),true)
+  SHELL                = /bin/bash $(MOD_SCRIPT_DIR)/timed-make-shell.sh
+endif
+
 MAKEFLAGS             += -r
 
 include $(MODDIR)/make/platform.mk
 include $(MODDIR)/make/projects.mk
 
-ifeq ($(MAKE_BENCHMARK),true)
-  SHELL                = $(MOD_SCRIPT_DIR)/timed-make-shell.sh
-endif
-
 # ----- pre-local.mk
 
 ifneq ($(wildcard $(MODDIR)/make/pre-local.mk),)
diff --git a/scripts/timed-make-shell.sh b/scripts/timed-make-shell.sh
index 653b7ce7..09001ed3 100644
--- a/scripts/timed-make-shell.sh
+++ b/scripts/timed-make-shell.sh
@@ -2,6 +2,5 @@
 
 shift  # get rid of the '-c' supplied by make.
 log=/tmp/make-cmds.log
-echo running "$*" >> $log
-time /bin/bash -c "$*" 2>&1 | tee -a $log
+/usr/bin/time --format "%E $*" -ao $log /bin/bash -c "$*"