diff --git a/reporting/timer b/reporting/timer index 479dcb6..3c1731c 100755 --- a/reporting/timer +++ b/reporting/timer @@ -28,4 +28,6 @@ function displaytime { while true; do displaytime "$SECONDS" >&2 sleep 1 + # die if parent dies + kill -0 $PPID 2>/dev/null || exit done