lib/scripts/showtime
author wenzelm
Fri, 13 Mar 1998 18:15:14 +0100
changeset 4744 4469d498cd48
parent 4450 2c64ce912684
child 9789 7e5e6c47c0b5
permissions -rwxr-xr-x
moved addsplits [expand_if] from HOL_basic_ss to HOL_ss;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4436
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset
     1
#!/bin/bash
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset
     2
#
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset
     3
# $Id$
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset
     4
#
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset
     5
# showtime - print time.
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset
     6
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset
     7
TIME=$1
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset
     8
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset
     9
SECS=$[ $TIME % 60 ]
4450
2c64ce912684 leading 0s;
wenzelm
parents: 4436
diff changeset
    10
[ $SECS -lt 10 ] && SECS=0$SECS
2c64ce912684 leading 0s;
wenzelm
parents: 4436
diff changeset
    11
4436
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset
    12
MINUTES=$[ ($TIME / 60) % 60 ]
4450
2c64ce912684 leading 0s;
wenzelm
parents: 4436
diff changeset
    13
[ $MINUTES -lt 10 ] && MINUTES=0$MINUTES
2c64ce912684 leading 0s;
wenzelm
parents: 4436
diff changeset
    14
4436
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset
    15
HOURS=$[ $TIME / 3600 ]
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset
    16
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset
    17
echo "${HOURS}:${MINUTES}:${SECS}"