osrm-backend/scripts/timer.sh
Daniel J. Hofmann ca21b8833a Removes Gnu Date Usage 👴
\U+1Fstallman-emoji
2016-10-19 18:26:20 +02:00

13 lines
228 B
Bash
Executable File

#!/bin/bash
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