grepping-through-time.sh

time sleep 1
  #     real	0m1.001s
  #     user	0m0.000s
  #     sys	0m0.001s


##
## What if I only care about the real time? Grepping fails?!
##

time sleep 1 | grep real
  #     real	0m1.001s
  #     user	0m0.000s
  #     sys	0m0.001s


##
## That's because it's because I must redirect STDERR to STDOUT...
## But this fails too...
##

time sleep 1 2>&1 | grep real
  #     real	0m1.001s
  #     user	0m0.000s
  #     sys	0m0.001s


##
## That's because time is a bash builtin, not affected by pipe redirection.
## But there's a proper command `/usr/bin/time`, which takes arguments specified in `man time`
##

/usr/bin/time -p sleep 1  2>&1 | grep real
  #     real	0m1.001s


##
## If we had pipes in the expression we wanted to time, we'd need to use the builtin.
## In this case, we can use a little subshell trick:
##

(time sleep 1) 2>&1 | grep real
  #    real	0m1.001s


##
## Of course `man bash` informs us there's an even simpler way to do the same thing.
##

TIMEFORMAT=%R ; time sleep 1 ; unset TIMEFORMAT
  #    1.001