On 07/08/24 at 21:57, Thomas Schmitt wrote:
The number formats are hardcoded:
https://sources.debian.org/src/time/1.9-0.2/src/time.c/#L526
case 'S': /* System time. */
fprintf (fp, "%ld.%02ld",
https://sources.debian.org/src/time/1.9-0.2/src/time.c/#L531
case 'U': /* User time. */
fprintf (fp, "%ld.%02ld",
https://sources.debian.org/src/time/1.9-0.2/src/time.c/#L552
case 'e': /* Elapsed real time in seconds. */
fprintf (fp, "%ld.%02ld",
There is no interpreter to see for adjustable number precision.
Thanks for the exhaustive answer, I was wondered that the /usr/bin/time
command has precision hardcoded in the sources :( which command has a
precision of at least 3 decimals to measure commands execution?
The Bash's shell keyword "time" it could be fine, but I don't know how
to redirect its output to a file (-o switch of /usr/bin/time).
Cheers
--
Franco Martelli
