#! /bin/bash
clear
mkdir -p logs

. setenv

if [ -z "$LOG_NAME" ] ; then LOG_NAME=-$1 ; fi
if [ "$LOG_NAME" = "-" ] ; then LOG_NAME="" ; fi

$(which time) -v -o logs/make$LOG_NAME.time make -C src/make "$@" 2>&1 | tee logs/make$LOG_NAME.log