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

Authored by wosch on Jul 2 2025, 1:46 PM.

Details

Reviewers

brooks
markj

Group Reviewers

srcmgr

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

Diff Detail

Lint

Lint Skipped

Unit

Tests Skipped

Event Timeline

wosch requested review of this revision.Jul 2 2025, 1:46 PM

wosch created this revision.

wosch added reviewers: brooks, markj.

wosch added a reviewer: srcmgr.

wosch mentioned this in D51119: Revert "src/Makefile: log real/user/system time for build targets".Jul 2 2025, 1:51 PM

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.

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

Revision Contents
Changeset List

Path

Size

Makefile

2 lines

Diff 157836

View Options

src/Makefile: write time logging to stderr instead of stdoutNeeds ReviewPublicActions