#!/bin/bash

shift  # get rid of the '-c' supplied by make.
echo running "$*" >>/tmp/make-cmds.log
time /bin/bash -c "$*"