From 153d2d8fd0284ded924f4f42f81c25b97a7dae77 Mon Sep 17 00:00:00 2001
From: Jan Lindemann <jan@janware.com>
Date: Fri, 19 Jun 2015 11:20:31 +0000
Subject: [PATCH] timed-make-shell.sh: Add timed-make-shell.sh

Signed-off-by: Jan Lindemann <jan@janware.com>
---
 scripts/timed-make-shell.sh | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 scripts/timed-make-shell.sh

diff --git a/scripts/timed-make-shell.sh b/scripts/timed-make-shell.sh
new file mode 100644
index 00000000..f890c9e6
--- /dev/null
+++ b/scripts/timed-make-shell.sh
@@ -0,0 +1,6 @@
+#!/bin/bash
+
+shift  # get rid of the '-c' supplied by make.
+echo running "$*" >>/tmp/make-cmds.log
+time /bin/bash -c "$*"
+