diff options
| author | letouzey | 2012-10-04 18:16:27 +0000 |
|---|---|---|
| committer | letouzey | 2012-10-04 18:16:27 +0000 |
| commit | 41451e5ec3136b153fcc5af00c8bb4af870a498c (patch) | |
| tree | 8e9f2207ddee7afb78c9fb794f7f082fd3049a76 /plugins/syntax | |
| parent | 88e15b0bd942b4a316afa660da04b6639bccd2dd (diff) | |
Makefile.build: easier compilation with timings info
On a reasonable platform equipped with a /usr/bin/time, a simple
"make TIMED=1" should provide you with timings of the .v compilations.
If you don't have /usr/bin/time, or prefer a different output format,
you can still do a "make TIMECMD='...'".
For storing the timings in a spreadsheet, simply do:
"make TIMED=1 2> timings.csv"
and then import this csv in your favorite office program,
with whitespace as separator.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15850 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions