From 9849b21d756f2603e57363124be83bd87ff33af6 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sun, 19 Apr 2020 14:17:58 -0400
Subject: 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.
---
 tools/CoqMakefile.in | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 0202b3136b..745bbb7e55 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -66,7 +66,7 @@ VERBOSE ?=
 TIMED?=
 TIMECMD?=
 # Use command time on linux, gtime on Mac OS
-TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)"
+TIMEFMT?="$@ (real: %e, user: %U, sys: %S, mem: %M ko)"
 ifneq (,$(TIMED))
 ifeq (0,$(shell command time -f "" true >/dev/null 2>/dev/null; echo $$?))
 STDTIME?=command time -f $(TIMEFMT)
-- 
cgit v1.2.3