osrm-backend/scripts/timer.sh
2016-10-21 17:56:56 +02:00

17 lines
283 B
Bash
Executable File

#!/usr/bin/env bash
set -o errexit
set -o pipefail
set -o nounset
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"
NEW_ENTRY="$NAME\t$TIME"
echo -e "$NEW_ENTRY" >> $TIMINGS_FILE