diff options
| author | Robert Norton | 2017-04-19 12:16:00 +0100 |
|---|---|---|
| committer | Robert Norton | 2017-04-20 11:06:05 +0100 |
| commit | d11cd6e87c635d843759d10f9173c1a28ff3c62b (patch) | |
| tree | 4bf98003feaeb9eb327ccca39be86e5a5f91e264 /src/reporting_basic.ml | |
| parent | 3ff6d30fe20aec5b690d61f5519d695f19094c52 (diff) | |
attempt to optimise performance if not tracing writes.
Diffstat (limited to 'src/reporting_basic.ml')
0 files changed, 0 insertions, 0 deletions