# HG changeset patch
# User wenzelm
# Date 1223061197 -7200
# Node ID 5175b022e21631a5cd12ff46611f7bf670b4d29b
# Parent  c5420429a5aa830cf576c1e1cb749c74b4725857
factor: proper padding of digits;

diff -r c5420429a5aa -r 5175b022e216 lib/scripts/timestop.bash
--- 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
 }