[minor] "precision" of $SECONDS

[Stephane Chazelas]

$ time bash -c 'while ((SECONDS < 1)); do :; done'
bash -c 'while ((SECONDS < 1)); do :; done'  0.39s user 0.00s system 99% cpu 
0.387 total

That can take in between 0 and 1 seconds. Or in other words,
$SECONDS becomes 1 in between 0 and 1 second after the shell was
started.

The reason seems to be because the shell records the value
returned by time() upon start-up and $SECONDS expands to
time()-that_saved_time. So, if bash is started at 10:00:00.999,
then $SECONDS will become 1 only a milisecond after startup
while if it's started at 10:00:01.000, $SECONDS will become 1 a
full second later.

IMO, it would be better if gettimeofday() or equivalent was used
instead of time() so that $SECONDS be incremented exactly one
second after start-up like ksh93 does.

mksh and zsh behave like bash (I'll raise the issue there as
well).

With zsh (like in ksh93), one can do "typeset -F SECONDS" to
make $SECONDS floating point, which can be used as a work around
of the "issue".

-- 
Stephane