diff options
| author | Gaëtan Gilbert | 2020-04-20 23:16:42 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-20 23:16:42 +0200 |
| commit | f6f789f577efec5cfcd16c98290dab81162aa64c (patch) | |
| tree | 817382b17554f7106e38b5083d2e5936419eae35 /tools | |
| parent | 51a938a260d989f11fb1cd1d7a0205c6183f3809 (diff) | |
| parent | 9849b21d756f2603e57363124be83bd87ff33af6 (diff) | |
Merge PR #12126: TIMEFMT: Display the output file name
Reviewed-by: SkySkimmer
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 2 |
1 files changed, 1 insertions, 1 deletions
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) |