isabelle: lib/scripts/timestart.bash@3a60518900e4 (annotated)

31310 b5365a9db718 uniform treatment of shellscript mode; wenzelm parents: 29145 diff changeset	1	# -- shell-script -- :mode=shellscript:
29145 b1c6f4563df7 removed Ids; wenzelm parents: 26576 diff changeset	2	#
18317 bab988e37393 timestart - setup bash environment for timing; wenzelm parents: diff changeset	3	# Author: Makarius
bab988e37393 timestart - setup bash environment for timing; wenzelm parents: diff changeset	4	#
bab988e37393 timestart - setup bash environment for timing; wenzelm parents: diff changeset	5	# timestart - setup bash environment for timing.
bab988e37393 timestart - setup bash environment for timing; wenzelm parents: diff changeset	6	#
bab988e37393 timestart - setup bash environment for timing; wenzelm parents: diff changeset	7
bab988e37393 timestart - setup bash environment for timing; wenzelm parents: diff changeset	8	TIMES_RESULT=""
bab988e37393 timestart - setup bash environment for timing; wenzelm parents: diff changeset	9
bab988e37393 timestart - setup bash environment for timing; wenzelm parents: diff changeset	10	function get_times () {
bab988e37393 timestart - setup bash environment for timing; wenzelm parents: diff changeset	11	local TMP="/tmp/get_times$$"
bab988e37393 timestart - setup bash environment for timing; wenzelm parents: diff changeset	12	times > "$TMP" # No pipe here!
26576 fc76b7b79ba9 removed obsolete AUTO_PERL feature; wenzelm parents: 18364 diff changeset	13	TIMES_RESULT="$SECONDS $(echo $(cat "$TMP") \| perl -pe 's,\d+m\d+\.\d+s \d+m\d+\.\d+s (\d+)m(\d+)\.\d+s +(\d+)m(\d+)\.\d+s, $1 * 60 + $2 + $3 * 60 + $4,e')"
18327 1ee4523c831f tuned; wenzelm parents: 18322 diff changeset	14	rm -f "$TMP"
18317 bab988e37393 timestart - setup bash environment for timing; wenzelm parents: diff changeset	15	}
bab988e37393 timestart - setup bash environment for timing; wenzelm parents: diff changeset	16
bab988e37393 timestart - setup bash environment for timing; wenzelm parents: diff changeset	17	get_times # sets TIMES_RESULT

author	krauss
	Mon, 28 Mar 2011 09:22:22 +0200
changeset 42140	3a60518900e4
parent 31310	b5365a9db718
child 58639	1df53737c59b
permissions	-rw-r--r--