diff options
author | bors[bot] <26634292+bors[bot]@users.noreply.github.com> | 2020-10-22 19:15:48 +0100 |
---|---|---|
committer | GitHub <[email protected]> | 2020-10-22 19:15:48 +0100 |
commit | edf46a13a6a28093985d2d934ef97570947b9494 (patch) | |
tree | 289604e28fdc5bd201086156e3e2b8aa30184c97 /docs/dev/guide.md | |
parent | 3d349597fd47dc76dcecfb7a56775fa02c7a6db7 (diff) | |
parent | b59a0dbf6a808ccba884fbb82ecb320e5bb2a6d1 (diff) | |
parent | 5f5b1ffdd16a6501865ca0c8c7c83b9e9777984d (diff) |
Merge #6325 #6327
6325: Add generated diagnostic docs to the manual r=matklad a=flodiebold
It seemed that we're not actually including the generated diagnostic docs anywhere yet? So I added something to the manual. This is completely untested though.
6327: Update debugging.md r=matklad a=stanciuadrian
`on_task` is no longer there.
I have used `on_request` instead.
Co-authored-by: Florian Diebold <[email protected]>
Co-authored-by: Adrian Stanciu <[email protected]>