diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-29 14:56:36 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-30 13:16:54 -0400 |
| commit | d83bd63441d313b6dabe71cae647b1950c621cf6 (patch) | |
| tree | 2651efaba54a87d1e1fb38cf28d94eae64722500 | |
| parent | 35e0f327405fb659c7ec5f9f7d26ea284aa45810 (diff) | |
Better support for make TIMED=1 on Windows
This fixes [bug #5619](https://coq.inria.fr/bugs/show_bug.cgi?id=5619)
| -rw-r--r-- | Makefile.build | 14 | ||||
| -rw-r--r-- | tools/CoqMakefile.in | 2 |
2 files changed, 8 insertions, 8 deletions
diff --git a/Makefile.build b/Makefile.build index 0dafde997..05d751f54 100644 --- a/Makefile.build +++ b/Makefile.build @@ -101,7 +101,7 @@ DEPENDENCIES := \ ########################################################################### # Default timing command -STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)" +STDTIME=/usr/bin/time -f "$* (real: %e, user: %U, sys: %S, mem: %M ko)" TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) @@ -275,7 +275,7 @@ grammar/grammar.cma : $(GRAMCMO) @touch grammar/test.mlp $(HIDE)$(GRAMC) -pp '$(CAMLP4O) -I $(MYCAMLP4LIB) $^ -impl' -impl grammar/test.mlp -o grammar/test @rm -f grammar/test.* grammar/test - $(SHOW)'OCAMLC -a $@' + $(SHOW)'OCAMLC -a $@' $(HIDE)$(GRAMC) $^ -linkall -a -o $@ ## Support of Camlp5 and Camlp5 @@ -307,7 +307,7 @@ coqbyte: $(COQTOPBYTE) $(CHICKENBYTE) ifeq ($(BEST),opt) $(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) - $(SHOW)'COQMKTOP -o $@' + $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) $(LINKMETADATA) -o $@ $(STRIP) $@ $(CODESIGN) $@ @@ -317,7 +317,7 @@ $(COQTOPEXE): $(COQTOPBYTE) endif $(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) - $(SHOW)'COQMKTOP -o $@' + $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -o $@ # coqmktop @@ -667,7 +667,7 @@ Makefile $(wildcard Makefile.*) config/Makefile : ; %: @echo "Error: no rule to make target $@ (or missing .PHONY)" && false -# For emacs: -# Local Variables: -# mode: makefile +# For emacs: +# Local Variables: +# mode: makefile # End: diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 7b01c1b66..06d4d0b5b 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -62,7 +62,7 @@ VERBOSE ?= # Time the Coq process (set to non empty), and how (see default value) TIMED?= TIMECMD?= -STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)" +STDTIME?=/usr/bin/time -f "$* (real: %e, user: %U, sys: %S, mem: %M ko)" # Coq binaries COQC ?= "$(COQBIN)coqc" |