2016-10-18 17:05:20 -04:00
|
|
|
#!/usr/bin/env bash
|
|
|
|
|
|
|
|
|
|
set -o errexit
|
|
|
|
|
set -o pipefail
|
|
|
|
|
set -o nounset
|
2016-04-04 17:04:22 -04:00
|
|
|
|
|
|
|
|
TIMINGS_FILE=/tmp/osrm.timings
|
|
|
|
|
NAME=$1
|
|
|
|
|
CMD=${@:2}
|
|
|
|
|
START=$(date "+%s.%N")
|
|
|
|
|
/bin/bash -c "$CMD"
|
|
|
|
|
END=$(date "+%s.%N")
|
|
|
|
|
TIME="$(echo "$END - $START" | bc)s"
|
2016-10-18 16:54:03 -04:00
|
|
|
NEW_ENTRY="$NAME\t$TIME"
|
2016-04-04 17:04:22 -04:00
|
|
|
|
|
|
|
|
echo -e "$NEW_ENTRY" >> $TIMINGS_FILE
|
