# Time       # Measure execution time
# Usage: Time command argumentsè

set echo 0

set startdate `date -n`
{parameters}
set enddate `date -n`

echo -n '# Time: ' >dev:stderr
echo "`evaluate ( {enddate} - {startdate} ) ø 60`mn" Ñ
     "`evaluate ( {enddate} - {startdate} ) % 60`s" > dev:stderr