diff options
| author | Hugo Herbelin | 2017-07-20 13:12:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-07-20 15:18:06 +0200 |
| commit | f6a4599b852a32351163eb272d14718e32b58cec (patch) | |
| tree | 7291894ed1e3bce921de3abdbbccb4ec32d918d7 /API | |
| parent | 4d4ec6a095d01b6117ac3682d8a7882b1a2520e7 (diff) | |
A less intrusive Profile.close_profile.
No need to call Gc functions nor Unix timing functions when there is
nothing to report.
Moreover, PMP observed problems with these functions in the
debugger. PMP also reported that Gc.minor takes some noticeable time,
so no need to trigger some when unneeded.
Diffstat (limited to 'API')
0 files changed, 0 insertions, 0 deletions