From a9ef936dd189b1a1343ea75cd6f1a4686322435a Mon Sep 17 00:00:00 2001 From: Ville Rantanen Date: Fri, 10 Jan 2020 13:33:14 +0200 Subject: [PATCH] some use cases in the help --- reporting/timer | 39 ++++++++++++++++++++++++++++++++++++--- 1 file changed, 36 insertions(+), 3 deletions(-) diff --git a/reporting/timer b/reporting/timer index 3c1731c..8cbc2f4 100755 --- a/reporting/timer +++ b/reporting/timer @@ -4,6 +4,17 @@ function helpexit() { echo "Simple Timer." echo '$PREFIX is printed before the time' echo '$POSTFIX is printed after the time' + echo 'Reset timer with kill -10' + echo ' + +# use cases: +# timer | sleep 10 +# +# timer & +# sleep 10; kill -10 %1; sleep 5; kill %1 +# +# PREFIX=$'"'"'\033[33;1m'"'"' POSTFIX=$'"'"'\033[0m'"'"' timer | sleep 5 +' exit } @@ -25,9 +36,31 @@ function displaytime { printf '%02d:%02d]%s\r' $M $S $POSTFIX } -while true; do +function finish_up { displaytime "$SECONDS" >&2 - sleep 1 + echo "" >&2 + exit +} + +function reset { + STARTED=$SECONDS +} + +trap finish_up EXIT 9 15 +trap reset 10 + +STARTED=$SECONDS +while true; do + # Were in terminal + if [[ -t 1 ]]; then printf '\033[s'; fi + displaytime $(( SECONDS - STARTED )) >&2 + if [[ -t 1 ]]; then printf '\033[u'; fi # die if parent dies - kill -0 $PPID 2>/dev/null || exit + kill -0 $PPID 2>/dev/null || { exit; } + # if stdout is pipe, print time there + # if pipe dies, timer dies too + if [[ ! -t 1 ]]; then displaytime "$SECONDS"; fi + sleep 1 done + +