diff --git a/reporting/timer b/reporting/timer index 8cbc2f4..d3bab7d 100755 --- a/reporting/timer +++ b/reporting/timer @@ -4,6 +4,7 @@ function helpexit() { echo "Simple Timer." echo '$PREFIX is printed before the time' echo '$POSTFIX is printed after the time' + echo '$TIMERPID is a PID number. When the process ends, timer ends.' echo 'Reset timer with kill -10' echo ' @@ -14,6 +15,11 @@ function helpexit() { # sleep 10; kill -10 %1; sleep 5; kill %1 # # PREFIX=$'"'"'\033[33;1m'"'"' POSTFIX=$'"'"'\033[0m'"'"' timer | sleep 5 +# +# sleep 4 & +# p=$! +# TIMERPID=$p timer & +# sleep 10 ' exit } @@ -37,6 +43,7 @@ function displaytime { } function finish_up { + echo "Timer terminated" >&2 displaytime "$SECONDS" >&2 echo "" >&2 exit @@ -60,6 +67,9 @@ while true; do # if stdout is pipe, print time there # if pipe dies, timer dies too if [[ ! -t 1 ]]; then displaytime "$SECONDS"; fi + if [[ -n "$TIMERPID" ]]; then + kill -0 "$TIMERPID" 2>/dev/null || { exit; } + fi sleep 1 done