suppress small CPU time, notably on x86-windows, where bash does not account for the poly process;

--- 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"