Re: Increasing "time" command precision

["Thomas Schmitt" <scdbackup@gmx.net>]

Hi,

it turns out that TIMEFORMAT belongs to the bash builtin "time"
and that digit precision numbers only up to 3 are obeyed.

  $ export TIMEFORMAT="r=%7R
  u=%4U
  s=%1S"
  $ time echo

  r=0.000
  u=0.000
  s=0.0
  $

man bash:

  %[p][l]R  The elapsed time in seconds.
  [...]
  The optional p is a digit specifying the precision, the number
  of fractional digits after a decimal point. A value of 0 causes
  no decimal point or fraction to be output. At most three places
  after the decimal point may be specified; values of p greater
  than 3 are changed to 3. If p is not specified, the value 3 is
  used.


Have a nice day :)

Thomas