Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
lib/scripts/showtime
author wenzelm
Wed, 25 Nov 1998 14:03:20 +0100
changeset 5961 6cf4e46ce95a
parent 4450 2c64ce912684
child 9789 7e5e6c47c0b5
permissions -rwxr-xr-x
replaced prs by std_output / writeln;
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$
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset 
     4
 
#
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset 
     5
 
# showtime - print time.
a3a683a8bcc6 showtime - print time.
wenzelm
parents:
diff changeset 
     6
 












a3a683a8bcc6
showtime - print time.



wenzelm


parents: 

diff
changeset




     7


TIME=$1













a3a683a8bcc6
showtime - print time.



wenzelm


parents: 

diff
changeset




     8














a3a683a8bcc6
showtime - print time.



wenzelm


parents: 

diff
changeset




     9


SECS=$[ $TIME % 60 ]








4450






2c64ce912684
leading 0s;



wenzelm


parents: 
4436

diff
changeset




    10


[ $SECS -lt 10 ] && SECS=0$SECS













2c64ce912684
leading 0s;



wenzelm


parents: 
4436

diff
changeset




    11









4436






a3a683a8bcc6
showtime - print time.



wenzelm


parents: 

diff
changeset




    12


MINUTES=$[ ($TIME / 60) % 60 ]








4450






2c64ce912684
leading 0s;



wenzelm


parents: 
4436

diff
changeset




    13


[ $MINUTES -lt 10 ] && MINUTES=0$MINUTES













2c64ce912684
leading 0s;



wenzelm


parents: 
4436

diff
changeset




    14









4436






a3a683a8bcc6
showtime - print time.



wenzelm


parents: 

diff
changeset




    15


HOURS=$[ $TIME / 3600 ]













a3a683a8bcc6
showtime - print time.



wenzelm


parents: 

diff
changeset




    16














a3a683a8bcc6
showtime - print time.



wenzelm


parents: 

diff
changeset




    17


echo "${HOURS}:${MINUTES}:${SECS}"















isabelle