# 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