Patch #645894: Use getrusage for computing the time consumption in
profile.py if available.
2 files changed