lib/scripts/timestop.bash
changeset 18322 56554bb23eda
parent 18318 deb87d7e44bc
child 28467 c8336c42668e
equal deleted inserted replaced
18321:3414557c2dda 18322:56554bb23eda
    11 {
    11 {
    12   local TIMES_START="$TIMES_RESULT"
    12   local TIMES_START="$TIMES_RESULT"
    13   get_times
    13   get_times
    14   local TIMES_STOP="$TIMES_RESULT"
    14   local TIMES_STOP="$TIMES_RESULT"
    15   local KIND
    15   local KIND
    16   for KIND in 1 2 3
    16   for KIND in 1 2
    17   do
    17   do
    18     local START=$(echo "$TIMES_START" | cut -d " " -f $KIND)
    18     local START=$(echo "$TIMES_START" | cut -d " " -f $KIND)
    19     local STOP=$(echo "$TIMES_STOP" | cut -d " " -f $KIND)
    19     local STOP=$(echo "$TIMES_STOP" | cut -d " " -f $KIND)
    20 
    20 
    21     local TIME=$[ $STOP - $START ]
    21     local TIME=$[ $STOP - $START ]
    25     [ $MINUTES -lt 10 ] && MINUTES="0$MINUTES"
    25     [ $MINUTES -lt 10 ] && MINUTES="0$MINUTES"
    26     local HOURS=$[ $TIME / 3600 ]
    26     local HOURS=$[ $TIME / 3600 ]
    27 
    27 
    28     local KIND_NAME
    28     local KIND_NAME
    29     [ "$KIND" = 1 ] && KIND_NAME="elapsed time"
    29     [ "$KIND" = 1 ] && KIND_NAME="elapsed time"
    30     [ "$KIND" = 2 ] && KIND_NAME="user"
    30     [ "$KIND" = 2 ] && KIND_NAME="cpu time"
    31     [ "$KIND" = 3 ] && KIND_NAME="system"
       
    32     local RESULT="${HOURS}:${MINUTES}:${SECS} ${KIND_NAME}"
    31     local RESULT="${HOURS}:${MINUTES}:${SECS} ${KIND_NAME}"
    33 
    32 
    34     if [ -z "$TIMES_REPORT" ]; then
    33     if [ -z "$TIMES_REPORT" ]; then
    35       TIMES_REPORT="$RESULT"
    34       TIMES_REPORT="$RESULT"
    36     else
    35     else