# HG changeset patch
# User wenzelm
# Date 1133459124 -3600
# Node ID 4365c8d84f69f633b70785fe0aa312cffa089ffb
# Parent  56554bb23eda50ba365e614f74a7984693987774
superceded by timestart|stop.bash;

diff -r 56554bb23eda -r 4365c8d84f69 lib/scripts/showtime
--- a/lib/scripts/showtime	Thu Dec 01 18:44:47 2005 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# showtime - print time.
-
-TIME="$1"
-
-SECS=$[ $TIME % 60 ]
-[ $SECS -lt 10 ] && SECS="0$SECS"
-
-MINUTES=$[ ($TIME / 60) % 60 ]
-[ $MINUTES -lt 10 ] && MINUTES="0$MINUTES"
-
-HOURS=$[ $TIME / 3600 ]
-
-echo "${HOURS}:${MINUTES}:${SECS}"