From 986aa3f7c85f973211d48f5b83cc2a0d0e42bb57 Mon Sep 17 00:00:00 2001 From: Ville Rantanen Date: Fri, 10 Jan 2020 12:44:23 +0200 Subject: [PATCH] die if parent of timer dies --- reporting/timer | 2 ++ 1 file changed, 2 insertions(+) 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