On Thu, Aug 8, 2024, 8:13 AM Greg Wooledge wrote:
> On Thu, Aug 08, 2024 at 15:08:33 +0200, Franco Martelli wrote:
> > 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).
>
> https://mywiki.wooledge.org/BashFAQ/
On Thu, Aug 08, 2024 at 15:08:33 +0200, Franco Martelli wrote:
> 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).
https://mywiki.wooledge.org/BashFAQ/032
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 '
Hi,
Greg Wooledge wrote:
> > > * TIMEFORMAT=... time foo will invoke /usr/bin/time, but
> > >TIMEFORMAT=... eval time foo will use the builtin.
I wrote:
> > I wonder about the formal reason for this.
> There are some mysteries in bash that I'm content simply to write off as
> "here b
On Thu, Aug 08, 2024 at 08:31:10 +0200, Thomas Schmitt wrote:
> Greg Wooledge wrote:
> > * TIMEFORMAT=... time foo will invoke /usr/bin/time, but
> >TIMEFORMAT=... eval time foo will use the builtin.
(Yeah, oops, time is a "shell keyword", not a "builtin".)
> I wonder about the formal
Hi,
Greg Wooledge wrote:
> * TIMEFORMAT=... time foo will invoke /usr/bin/time, but
>TIMEFORMAT=... eval time foo will use the builtin.
I wonder about the formal reason for this.
Is it because "time" is not listed in the man page under
SHELL BUILTIN COMMANDS but mentioned as "reserve
On Wed, Aug 07, 2024 at 22:15:00 +0200, Thomas Schmitt wrote:
> 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
Ju
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
Hi,
Franco Martelli wrote:
> ~# export TIMEFORMAT='real%3R
> user%3U
> sys %3S'
The manual and the source code say that the format variable is "TIME"
not "TIMEFORMAT".
https://sources.debian.org/src/time/1.9-0.2/src/time.c/#L656
It seems to understand the two characters "\n" as lin
9 matches
Mail list logo
