diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-07-07 09:34:54 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-07-07 09:34:54 +0200 |
| commit | 64dd31dbc8117794be16921899ff1716a5223060 (patch) | |
| tree | e9d07126010061e2c44f73de21f5c1339d611fc3 /tools | |
| parent | f896d7cbfd22713e434d6de74e973a2ed1195913 (diff) | |
| parent | d83bd63441d313b6dabe71cae647b1950c621cf6 (diff) | |
Merge PR #844: Better support for make TIMED=1 on Windows
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index c4afc930a..86be54d46 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" |