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

(limited to 'tools')

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
-- 
cgit v1.2.3