diff options
| author | bors[bot] <bors[bot]@users.noreply.github.com> | 2019-05-05 17:02:19 +0100 |
|---|---|---|
| committer | bors[bot] <bors[bot]@users.noreply.github.com> | 2019-05-05 17:02:19 +0100 |
| commit | 3ea25a66a8deab9e20654dbc8d2bf07df2cbb6f8 (patch) | |
| tree | 0bd7f6aba3d7486fc0e99437888792b572532010 /docs/user | |
| parent | 9c302980e386734472f9bae50a0db59247cba623 (diff) | |
| parent | 7e7ea0e79dc70fc45aa2bf51f210aaaaf2208060 (diff) | |
Merge #1245
1245: Add profiling to diagnostics r=matklad a=marcogroppo
Add profiling to `diagnostics()` - see #1244.
Co-authored-by: Marco Groppo <[email protected]>
Diffstat (limited to 'docs/user')
0 files changed, 0 insertions, 0 deletions