isabelle: lib/scripts/showtime@7b2be4d2703a (annotated)

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 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	kleing
	Fri, 22 Sep 2000 13:13:15 +0200
changeset 10058	7b2be4d2703a
parent 9789	7e5e6c47c0b5
child 10555	2323ec838401
permissions	-rwxr-xr-x