die if parent of timer dies

2020-01-10 12:44:23 +02:00
parent 5f5c24641e
commit 986aa3f7c8
1 changed files with 2 additions and 0 deletions
--- 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