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