isabelle: lib/scripts/timestart.bash@87c132cf5860 (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 () {
58639 1df53737c59b prefer Unix standard-conformant $TMPDIR over hard-wired /tmp; wenzelm parents: 31310 diff changeset	11	local TMP="${TMPDIR:-/tmp}/get_times$$"
18317 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	wenzelm
	Tue, 05 Nov 2019 14:28:00 +0100
changeset 71047	87c132cf5860
parent 58639	1df53737c59b
permissions	-rw-r--r--