| changeset 18323 | 4365c8d84f69 |
| parent 18322 | 56554bb23eda |
| child 18324 | d1c4b1112e33 |
| 18322:56554bb23eda | 18323:4365c8d84f69 |
|---|---|
1 #!/usr/bin/env bash |
|
2 # |
|
3 # $Id$ |
|
4 # Author: Markus Wenzel, TU Muenchen |
|
5 # |
|
6 # showtime - print time. |
|
7 |
|
8 TIME="$1" |
|
9 |
|
10 SECS=$[ $TIME % 60 ] |
|
11 [ $SECS -lt 10 ] && SECS="0$SECS" |
|
12 |
|
13 MINUTES=$[ ($TIME / 60) % 60 ] |
|
14 [ $MINUTES -lt 10 ] && MINUTES="0$MINUTES" |
|
15 |
|
16 HOURS=$[ $TIME / 3600 ] |
|
17 |
|
18 echo "${HOURS}:${MINUTES}:${SECS}" |