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
