Merge PR #12125: Fix Makefile warning: undefined variable '*'

Reviewed-by: SkySkimmer

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