How to change default time display format (and buglet?)?

OK, this is silly:

test=# select date_trunc('microseconds', TIME '17:12:28.125);
date_trunc
-------------
17:12:28.12
(1 row)

Surely one hundred and twenty three microseconds is a valid fraction of a second? Surely the default format should use microseconds and not hundreds of seconds? And even if it should use 1/100 seconds, surely it should do the rounding right? (No, it does not appear to be a floating point error:

test=# select date_part('microseconds', date_trunc('microseconds', TIME '17:12:28.125'));
date_part
-----------
28125000
(1 row)

even though adding a little helps:

test=# select date_trunc('microseconds', TIME '17:12:28.125001');
date_trunc
-------------
17:12:28.13
(1 row)
).

--- Allan.