Bash time (wrt: TIMEFORMAT) display: rounding vs. truncation?

[L. Walsh]

A bit of a "nit" :-). I noticed that the output of the Bash
builtin "time" function (Bash 3) is "truncated", not rounded. 

This might be personal preference, but rounding would seem
"less surprising" and of more interest.  I.e., if someone
displays a program's run-time, it seems rounding would
be more likely to give a "useful" answer.

Example:

1) TIMEFORMAT=" %2Rreal"; time usleep 90000
0.09real   <= expected (ignoring overhead)

2) TIMEFORMAT=" %1Rreal"; time usleep 90000
0.0real    <= not so useful; 0.1 would be better

3) TIMEFORMAT=" %0Rreal"; time usleep 990000   <= How close to 1sec**?
0real      <= ~999ms: missed it by "><" [that] much.

4) TIMEFORMAT=" %0Rreal"; time usleep 673000  <= About how long?
0real      <= 1 second would feel "closer", though admittedly,
              feelings are subjective: even with a "TF" of
              "%2R seconds", the resultant
0.68 seconds  is "nearly an eternity"***, to some. Truncating
              it to 0 doesn't seem intuitive.


Anyone else have any ideas or opinions on this?
Linda



**-w/overhead & TF="%Rreal":0.999real

***-"for an android"; :-)