diff -r 4b62e0cb3aa8 -r bab988e37393 lib/scripts/timestart.bash
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/timestart.bash	Thu Dec 01 18:37:22 2005 +0100
@@ -0,0 +1,21 @@
+# -*- shell-script -*-
+# $Id$
+# Author: Makarius
+#
+# timestart - setup bash environment for timing.
+#
+
+TIMES_RESULT=""
+
+#set by configure
+AUTO_PERL=perl
+
+function get_times () {
+  local TMP="/tmp/get_times$$"
+  times > "$TMP"   # No pipe here!
+  TIMES_RESULT="$SECONDS $(tail -1 "$TMP" | "$AUTO_PERL" -pe 's,(\d+)m(\d+)\.\d+s, $1 * 60 + $2,ge')"
+  /bin/rm -f "$TMP"
+}
+
+get_times  # sets TIMES_RESULT
+