Re: timevar: further work

[Bruno Haible]

> So, very obviously, the resolution of times() is 20 milliseconds (!).

Oops. It is 10 milliseconds, not 20 milliseconds. But that does not
change the conclusion.

Bruno