isabelle: lib/scripts/showtime@e4d8dea6dfc2 (annotated)

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 7e5e6c47c0b5 GPLed; wenzelm parents: 4450 diff changeset	4	# Author: Markus Wenzel, TU Muenchen
7e5e6c47c0b5 GPLed; 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 7e5e6c47c0b5 GPLed; 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 7e5e6c47c0b5 GPLed; 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 7e5e6c47c0b5 GPLed; 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}"

author	paulson
	Thu, 20 Feb 2003 11:09:48 +0100
changeset 13824	e4d8dea6dfc2
parent 10555	2323ec838401
child 14981	e73f8140af78
permissions	-rwxr-xr-x