diff options
| author | Maxime Dénès | 2017-07-11 14:44:59 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-07-11 14:44:59 +0200 |
| commit | 0986ee250818a5cb517b5e59fbd31e2cd1667775 (patch) | |
| tree | 01d38409f9db6202aabe16249df7d489cd853920 /tools | |
| parent | b5ad6a80107f196fa8ffcc4f5dff58bea8c4f70e (diff) | |
| parent | 032e4f2bf5cb6eadba6ebbb16dd5d0c812dd2033 (diff) | |
Merge branch 'v8.7'
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 c4afc930a7..86be54d462 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" |