src/Makefile: write time logging to stderr instead of stdout

[wosch]

Summary

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

[markj]

I don't think this is really right. Some top-level make targets are designed to be consumed by other programs, especially the ones I listed in D51119. It simply doesn't make sense to print the time for those targets on every invocation.

[brooks]

I have concerns about the implementation:

• I'm not sure we can count on /usr/bin/time existing on non-FreeBSD systems. At a minimum time_cmd should be overridable, but should really be optional
• -o is non-portable so this probably breaks cross builds
• I'm not thrilled about leaking tmp files every time the user interrupts a build