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 oheimb
Wed, 12 Aug 1998 16:21:18 +0200
changeset 5304 c133f16febc7
parent 4450 2c64ce912684
child 9789 7e5e6c47c0b5
permissions -rwxr-xr-x
the splitter is now defined as a functor moved addsplits, delsplits, Addsplits, Delsplits to Provers/splitter.ML moved split_thm_info to Provers/splitter.ML definined atomize via general mk_atomize removed superfluous rot_eq_tac from simplifier.ML HOL/simpdata.ML: renamed mk_meta_eq to meta_eq, re-renamed mk_meta_eq_simp to mk_meta_eq added Eps_eq to simpset
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