#Purpose:
#  Explore various ways to time command.

.PHONY: time show
TIME.format:='\nreal\t%4lR'
#Used as value of TIMEFORMAT below.
#See https://www.gnu.org/software/bash/manual/html_node/Bash-Variables.html
#  and search for TIMEFORMAT for possible values.
#  ***HOWEVER*** that doc says, at most, 3 decimal places are allowed.
#  IOW '%4R' means the same as '%3R' :(
#################
#following based on:
#  http://unix.stackexchange.com/questions/70653/increase-e-precision-with-usr-bin-time-shell-command
#  http://mywiki.wooledge.org/BashFAQ/032
#    especially the Pipe: example with
#    comment # Keep stdout and stderr unmolested
########################################  
SHELL:=/bin/bash
#^to enable use of TIMEFORMAT below.
.ONESHELL:
STRIP_NL:=perl -pe "chomp;"

time:
	echo -n "address@hidden">time.out
	TIMEFORMAT=$'\nreal\t%1R'
	{ time sleep .22222 ; } 2>&1 | $(STRIP_NL) >>time.out
	echo "}$@">>time.out
show:time
	@echo "+++$@:"
	@cat time.out
	@echo "---$@:"