lib/scripts/timestop.bash
changeset 28492 5175b022e216
parent 28469 0946c81ab77b
child 29145 b1c6f4563df7
--- a/lib/scripts/timestop.bash	Fri Oct 03 21:06:39 2008 +0200
+++ b/lib/scripts/timestop.bash	Fri Oct 03 21:13:17 2008 +0200
@@ -45,6 +45,7 @@
     local FACTOR=$(( $TIME2 * 100 / $TIME1 ))
     local FACTOR1=$(( $FACTOR / 100 ))
     local FACTOR2=$(( $FACTOR % 100 ))
+    if let "$FACTOR2 < 10"; then FACTOR2="0$FACTOR2"; fi
     TIMES_REPORT="$TIMES_REPORT, factor ${FACTOR1}.${FACTOR2}"
   fi
 }