lib/scripts/timestart.bash
changeset 29145 b1c6f4563df7
parent 26576 fc76b7b79ba9
child 31310 b5365a9db718
--- a/lib/scripts/timestart.bash	Sat Dec 20 11:39:34 2008 +0100
+++ b/lib/scripts/timestart.bash	Sat Dec 20 11:55:34 2008 +0100
@@ -1,5 +1,5 @@
 # -*- shell-script -*-
-# $Id$
+#
 # Author: Makarius
 #
 # timestart - setup bash environment for timing.