# HG changeset patch
# User wenzelm
# Date 1222984330 -7200
# Node ID 0946c81ab77b62e28c1d99fc7f71147dce47049e
# Parent  7c80ab57f56df895a57f584f290de5d6ddb1d640
time factor: one more digit;

diff -r 7c80ab57f56d -r 0946c81ab77b lib/scripts/timestop.bash
--- a/lib/scripts/timestop.bash	Thu Oct 02 23:30:44 2008 +0200
+++ b/lib/scripts/timestop.bash	Thu Oct 02 23:52:10 2008 +0200
@@ -42,9 +42,9 @@
   done
   if let "$TIME1 >= 5 && $TIME2 >= 5"
   then
-    local FACTOR=$(( $TIME2 * 10 / $TIME1 ))
-    local FACTOR1=$(( $FACTOR / 10 ))
-    local FACTOR2=$(( $FACTOR % 10 ))
+    local FACTOR=$(( $TIME2 * 100 / $TIME1 ))
+    local FACTOR1=$(( $FACTOR / 100 ))
+    local FACTOR2=$(( $FACTOR % 100 ))
     TIMES_REPORT="$TIMES_REPORT, factor ${FACTOR1}.${FACTOR2}"
   fi
 }