From 4ae8c7695976f803d9db1471bb00bf82c918a481 Mon Sep 17 00:00:00 2001
From: Eric House <eehouse@eehouse.org>
Date: Mon, 24 Jan 2011 22:19:02 -0800
Subject: [PATCH] break printed runtime into hours:minutes:seconds

---
 xwords4/linux/scripts/discon_ok2.sh | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/xwords4/linux/scripts/discon_ok2.sh b/xwords4/linux/scripts/discon_ok2.sh
index 09f85ae69..6565c8806 100755
--- a/xwords4/linux/scripts/discon_ok2.sh
+++ b/xwords4/linux/scripts/discon_ok2.sh
@@ -241,7 +241,7 @@ run_cmds() {
             PIDS[$KEY]=$!
         else
             sleep 2             # make sure it's had some time
-            kill ${PIDS[$KEY]}
+            kill ${PIDS[$KEY]} || true
             PIDS[$KEY]=0
             check_game $KEY
         fi
@@ -268,4 +268,10 @@ run_cmds
 print_stats
 
 wait
-echo "*********$0 finished: $(date) (took $(($(date +%s)-$STARTTIME)) seconds)**************"
+
+SECONDS=$(($(date +%s)-$STARTTIME))
+HOURS=$((SECONDS/3600))
+SECONDS=$((SECONDS%3600))
+MINUTES=$((SECONDS/60))
+SECONDS=$((SECONDS%60))
+echo "*********$0 finished: $(date) (took $HOURS:$MINUTES:$SECONDS)**************"