aboutsummaryrefslogtreecommitdiff
path: root/Makefile.dev
diff options
context:
space:
mode:
authorJason Gross2020-04-19 14:17:58 -0400
committerJason Gross2020-04-20 12:32:53 -0400
commit9849b21d756f2603e57363124be83bd87ff33af6 (patch)
tree84f25f6c223e6d1484d574379e9ddaee1161a129 /Makefile.dev
parent1a607cd9ff831e5393ec7eff8317ca4161161453 (diff)
TIMEFMT: Display the output file name
We now use `$@` rather than `$*` so that we display the output target rather than the stem of the rule. This is more consistent for rules that users add (where the pattern variable might be something insufficiently identifying), and also generalizes more nicely to mixing multiple compilers (we get a clear difference between producing OCaml files and producing .vo files, even if the filename is the same up to the suffix). The result is that it's easy to describe what the timing information of the build log records: each time comes with a label which is a file name, and the time is the time it takes to produce that file.
Diffstat (limited to 'Makefile.dev')
0 files changed, 0 insertions, 0 deletions