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`).
---
 Makefile.build                                                 |  4 ++--
 .../coq-makefile/timing/after/time-of-build-after.log.desired  | 10 ----------
 .../coq-makefile/timing/after/time-of-build-before.log.desired | 10 ----------
 test-suite/coq-makefile/timing/run.sh                          |  2 +-
 tools/CoqMakefile.in                                           |  4 ++--
 5 files changed, 5 insertions(+), 25 deletions(-)

diff --git a/Makefile.build b/Makefile.build
index 5b26f11b12..7879580e18 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -203,10 +203,10 @@ DEPENDENCIES := \
 # Use /usr/bin/env time on linux, gtime on Mac OS
 TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)"
 ifneq (,$(TIMED))
-ifeq (0,$(shell /usr/bin/env time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?))
+ifeq (0,$(shell /usr/bin/env time -f "" true >/dev/null 2>/dev/null; echo $$?))
 STDTIME?=/usr/bin/env 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?=time
diff --git a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired
index 7900c034da..4381160a4e 100644
--- a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired
+++ b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired
@@ -1,15 +1,5 @@
-Makefile:69: warning: undefined variable '*'
-Makefile:204: warning: undefined variable 'DSTROOT'
 COQDEP VFILES
-Makefile:69: warning: undefined variable '*'
-Makefile:204: warning: undefined variable 'DSTROOT'
-Makefile:69: warning: undefined variable '*'
-Makefile:204: warning: undefined variable 'DSTROOT'
-Makefile:69: warning: undefined variable '*'
-Makefile:204: warning: undefined variable 'DSTROOT'
 COQC Slow.v
 Slow (real: 0.04, user: 0.02, sys: 0.01, mem: 45512 ko)
 COQC Fast.v
 Fast (real: 0.41, user: 0.37, sys: 0.04, mem: 395200 ko)
-Makefile:69: warning: undefined variable '*'
-Makefile:204: warning: undefined variable 'DSTROOT'
diff --git a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired
index 7ab0bc75d9..e6af909268 100644
--- a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired
+++ b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired
@@ -1,15 +1,5 @@
-Makefile:69: warning: undefined variable '*'
-Makefile:204: warning: undefined variable 'DSTROOT'
 COQDEP VFILES
-Makefile:69: warning: undefined variable '*'
-Makefile:204: warning: undefined variable 'DSTROOT'
-Makefile:69: warning: undefined variable '*'
-Makefile:204: warning: undefined variable 'DSTROOT'
-Makefile:69: warning: undefined variable '*'
-Makefile:204: warning: undefined variable 'DSTROOT'
 COQC Slow.v
 Slow (real: 0.40, user: 0.35, sys: 0.04, mem: 394968 ko)
 COQC Fast.v
 Fast (real: 0.04, user: 0.03, sys: 0.00, mem: 46564 ko)
-Makefile:69: warning: undefined variable '*'
-Makefile:204: warning: undefined variable 'DSTROOT'
diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh
index 4ee4aae36c..f556638640 100755
--- a/test-suite/coq-makefile/timing/run.sh
+++ b/test-suite/coq-makefile/timing/run.sh
@@ -63,7 +63,7 @@ TO_SED_IN_PER_LINE=(
 
 for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do
   for ext in "" .desired; do
-    grep -v 'warning: undefined variable' < ${file}${ext} | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_FILE[@]}" > ${file}${ext}.processed
+    sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_FILE[@]}" ${file}${ext} > ${file}${ext}.processed
   done
   echo "cat $file"
   cat "$file"
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