Write time logging to stderr instead of stdout. This solves a problem that some users parse the output of make, as make makeman'. This is in line with the usual usage of time(1) command time make .... ' which displays the time to stderr.
/usr/bin/time make showconfig | wc
0.98 real 0.60 user 0.41 sys 244 741 5848
PR: 287274