isabelle: lib/scripts/showtime@56554bb23eda (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
4436 a3a683a8bcc6 showtime - print time. wenzelm parents: diff changeset	5	#
a3a683a8bcc6 showtime - print time. wenzelm parents: diff changeset	6	# showtime - print time.
a3a683a8bcc6 showtime - print time. wenzelm parents: diff changeset	7
9789 7e5e6c47c0b5 GPLed; wenzelm parents: 4450 diff changeset	8	TIME="$1"
4436 a3a683a8bcc6 showtime - print time. wenzelm parents: diff changeset	9
a3a683a8bcc6 showtime - print time. wenzelm parents: diff changeset	10	SECS=$[ $TIME % 60 ]
9789 7e5e6c47c0b5 GPLed; wenzelm parents: 4450 diff changeset	11	[ $SECS -lt 10 ] && SECS="0$SECS"
4450 2c64ce912684 leading 0s; wenzelm parents: 4436 diff changeset	12
4436 a3a683a8bcc6 showtime - print time. wenzelm parents: diff changeset	13	MINUTES=$[ ($TIME / 60) % 60 ]
9789 7e5e6c47c0b5 GPLed; wenzelm parents: 4450 diff changeset	14	[ $MINUTES -lt 10 ] && MINUTES="0$MINUTES"
4450 2c64ce912684 leading 0s; wenzelm parents: 4436 diff changeset	15
4436 a3a683a8bcc6 showtime - print time. wenzelm parents: diff changeset	16	HOURS=$[ $TIME / 3600 ]
a3a683a8bcc6 showtime - print time. wenzelm parents: diff changeset	17
a3a683a8bcc6 showtime - print time. wenzelm parents: diff changeset	18	echo "${HOURS}:${MINUTES}:${SECS}"

author	wenzelm
	Thu, 01 Dec 2005 18:44:47 +0100
changeset 18322	56554bb23eda
parent 14981	e73f8140af78
permissions	-rwxr-xr-x