Re: Increasing "time" command precision

[Franco Martelli <martellif67@gmail.com>]

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