[Speed] Tracking memory usage

[Armin Rigo]

Hi Victor,

Fwiw, there is some per-OS (and even apparently
per-Linux-distribution) solution mentioned here:
http://stackoverflow.com/questions/774556/peak-memory-usage-of-a-linux-unix-process

For me on Arch Linux, "/usr/bin/time -v CMD" returns a reasonable
value in "Maximum resident set size (kbytes)".  I guess that on OSes
where this works, it gives a zero-overhead, exact answer.


A bientôt,

Armin.