# HG changeset patch
# User wenzelm
# Date 1440092006 -7200
# Node ID 07592e2171801e67eaab53f37fb68cb99ae0e46f
# Parent  c967d423953a051486e40c47d9e4de419e290308
suppress small CPU time, notably on x86-windows, where bash does not account for the poly process;

diff -r c967d423953a -r 07592e217180 lib/scripts/timestop.bash
--- a/lib/scripts/timestop.bash	Thu Aug 20 19:19:19 2015 +0200
+++ b/lib/scripts/timestop.bash	Thu Aug 20 19:33:26 2015 +0200
@@ -34,10 +34,12 @@
     [ "$KIND" = 2 ] && KIND_NAME="cpu time"
     local RESULT="${HOURS}:${MINUTES}:${SECS} ${KIND_NAME}"
 
-    if [ -z "$TIMES_REPORT" ]; then
-      TIMES_REPORT="$RESULT"
-    else
-      TIMES_REPORT="$TIMES_REPORT, $RESULT"
+    if [ ${KIND} -eq 1 -o ${TIME} -ge 5 ]; then
+      if [ -z "$TIMES_REPORT" ]; then
+        TIMES_REPORT="$RESULT"
+      else
+        TIMES_REPORT="$TIMES_REPORT, $RESULT"
+      fi
     fi
   done
   if let "$TIME1 >= 5 && $TIME2 >= 5"