Hello,
I've installed the "time" package, I'd like to increase the number of
decimals in the output (say 3) but I got only 2 decimals.
Here what I tried:
~# export TIMEFORMAT='real %3R
user %3U
sys %3S'
~# /usr/bin/time -o elapsed ls -l
...
~# cat elapsed
0.00user 0.00system 0:00.00elapsed 100%CPU (0avgtext+0avgdata
3156maxresident)k
0inputs+0outputs (0major+147minor)pagefaults 0swaps
Is there a way to increase the precision of the time command? e.g.
0.000user 0.000system ...
Thanks for any hint
Cheers
--
Franco Martelli
