diff options
| author | Gaëtan Gilbert | 2020-04-20 13:21:25 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-20 13:21:25 +0200 |
| commit | b669ca8459f5d0fec2201c494d88c7d516c37be0 (patch) | |
| tree | 94f96d958508e1db7e518257c1024d3cb463b12d /tools | |
| parent | e77b7aed145718b73ca58c75bc7ed01d2b55446f (diff) | |
| parent | ff293b3564efec8c911c3df9cd3a71863161d8b3 (diff) | |
Merge PR #12125: Fix Makefile warning: undefined variable '*'
Reviewed-by: SkySkimmer
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 597351db9b..0202b3136b 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -68,10 +68,10 @@ TIMECMD?= # Use command time on linux, gtime on Mac OS TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)" ifneq (,$(TIMED)) -ifeq (0,$(shell command time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) +ifeq (0,$(shell command time -f "" true >/dev/null 2>/dev/null; echo $$?)) STDTIME?=command time -f $(TIMEFMT) else -ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) +ifeq (0,$(shell gtime -f "" true >/dev/null 2>/dev/null; echo $$?)) STDTIME?=gtime -f $(TIMEFMT) else STDTIME?=command time |