From 5ca33dcd307ce331964a2e9867e03218c6de621b Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 5 Jan 2010 15:24:45 +0000
Subject: use TIMECMD instead of TIME in makefile (unix cmd time reads its
 format in TIME)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12628 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile.build | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/Makefile.build b/Makefile.build
index 4b9dd34f42..73a98363dd 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -78,9 +78,13 @@ COQ_XML=	# is "-xml" when building XML library
 VM=		# is "-no-vm" to not use the vm"
 UNBOXEDVALUES=	# is "-unboxed-values" to use unboxed values
 COQOPTS=$(COQ_XML) $(VM) $(UNBOXEDVALUES)
-TIME=		# is "'time -p'" to get compilation time of .v 
+TIMECMD=	# is "'time -p'" to get compilation time of .v
 
-BOOTCOQTOP:=$(TIME) $(BESTCOQTOP) -boot $(COQOPTS)
+# NB: variable TIME, if set, is the formatting string for unix command 'time'.
+# For instance:
+# TIME="%C (%U user, %S sys, %e total, %M maxres)"
+
+BOOTCOQTOP:=$(TIMECMD) $(BESTCOQTOP) -boot $(COQOPTS)
 
 ###########################################################################
 # Infrastructure for the rest of the Makefile
-- 
cgit v1.2.3