isabelle: lib/scripts/showtime@10c51288b00d (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	wenzelm
	Sat, 03 Feb 2001 17:43:05 +0100
changeset 11047	10c51288b00d
parent 10555	2323ec838401
child 14981	e73f8140af78
permissions	-rwxr-xr-x