[wp-hackers] $precision in timer_stop unused

[Robert Deaton]

Wasn't sure if anyone else has noticed this, but for the last few
months there has been a $precision arguement for timer_stop that is
unused. Dunno if a bug report should be filed or if a dev will just
make the necessary changes (could just remove it since apparently
nobody is missing it anyways).

If a bug report needs to be filed, would one of you mind doing it for
me, I'm rather busy lately..