tools/Time


1
2
3
4
5
6
7
8
9
10

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

set echo 0

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

echo "# Time: `evaluate {enddate} - {startdate}` s" > dev:stderr