#! /bin/sh
# $Id$

args=""
if [ "$1" = "-a" ];then
	args="$args $1"
	shift
fi
(
	set -ex
	time nice make "$@"
	) 2>&1|tee $args errs2