fsfe-website/tools/inc_profiling.sh

32 lines
646 B
Bash

if [ -z "$inc_profiling" ]
then
inc_profiling=true
declare -A TIMER_START
prof_start()
# prof_start ID
# Start timer for ID
{
if [ -n "$PROFILE" ]
then
local id="$1"
TIMER_START[$id]=$( date +%s.%n )
fi
}
prof_elapsed()
# prof_elapsed ID [LABEL]
# Print elapsed time for timer ID.
# Optionally, a user-friendly LABEL can be supplied to be displayed instead of the ID.
{
if [ -n "$PROFILE" ]
then
local id="$1"
local label="${2:-$id}"
local timer_end=$( date +%s.%N )
local elapsed=$(echo "$timer_end - ${TIMER_START[$id]}" | bc -l)
echo "Elapsed time ($label): ${elapsed%%???????} seconds"
fi
}
fi