lib/scripts/showtime
author wenzelm
Fri, 10 Nov 2000 19:02:37 +0100
changeset 10432 3dfbc913d184
parent 9789 7e5e6c47c0b5
child 10555 2323ec838401
permissions -rwxr-xr-x
added axclass inverse and consts inverse, divide (infix "/"); moved axclass power to Nat.thy;
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$
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}"