diff options
| author | Jason Gross | 2020-04-19 14:17:58 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-04-19 14:43:55 -0400 |
| commit | ff293b3564efec8c911c3df9cd3a71863161d8b3 (patch) | |
| tree | b4d3c9825176246197140239d211de9b8e6b9907 /tools | |
| parent | 8d3f4fcd162c7dd23619f605d55e9a773c131e0e (diff) | |
Fix Makefile warning: undefined variable '*'
We fix
```
Makefile.build:222: warning: undefined variable '*'
```
by not passing a time format including a Makefile variable when not
inside a target (and whether or not the command succeeds should not
depend on the particular format in any case, and all we are testing for
is whether or not the command exists and supports `-f`).
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 |