lib/scripts/showtime
author wenzelm
Tue, 13 Feb 2001 16:31:18 +0100
changeset 11109 ce1cefc6c14c
parent 10555 2323ec838401
child 14981 e73f8140af78
permissions -rwxr-xr-x
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10555
2323ec838401 /usr/bin/env bash;
wenzelm
parents: 9789
diff changeset
     1
#!/usr/bin/env bash
4436
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset
     2
#
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset
     3
# $Id$
9789
wenzelm
parents: 4450
diff changeset
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm
parents: 4450
diff changeset
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
4436
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset
     6
#
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset
     7
# showtime - print time.
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset
     8
9789
wenzelm
parents: 4450
diff changeset
     9
TIME="$1"
4436
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset
    10
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset
    11
SECS=$[ $TIME % 60 ]
9789
wenzelm
parents: 4450
diff changeset
    12
[ $SECS -lt 10 ] && SECS="0$SECS"
4450
2c64ce912684 leading 0s;
wenzelm
parents: 4436
diff changeset
    13
4436
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset
    14
MINUTES=$[ ($TIME / 60) % 60 ]
9789
wenzelm
parents: 4450
diff changeset
    15
[ $MINUTES -lt 10 ] && MINUTES="0$MINUTES"
4450
2c64ce912684 leading 0s;
wenzelm
parents: 4436
diff changeset
    16
4436
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset
    17
HOURS=$[ $TIME / 3600 ]
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset
    18
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset
    19
echo "${HOURS}:${MINUTES}:${SECS}"