diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-05 15:24:45 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-05 15:24:45 +0000 |
| commit | 5ca33dcd307ce331964a2e9867e03218c6de621b (patch) | |
| tree | 97c53600044439310a326802e0358f6e47c9296e | |
| parent | ae3c06fdcbed65174b0a1ca88886a8c25bf45312 (diff) | |
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
| -rw-r--r-- | Makefile.build | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build index 4b9dd34f4..73a98363d 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 |