diff options
| author | bors[bot] <26634292+bors[bot]@users.noreply.github.com> | 2023-02-01 00:18:01 +0000 |
|---|---|---|
| committer | GitHub <[email protected]> | 2023-02-01 00:18:01 +0000 |
| commit | 594969f2811b53741d1c5e477350dbf5b1b24a9d (patch) | |
| tree | ce14e014dfbe8c3764040d7f9f1ffee84ab5747b /docs | |
| parent | 4c1946454874597c358e7c7d5bf555b687376a5b (diff) | |
| parent | b5cf332cc076a0de11ce6a0563a2235c9e57eb5c (diff) | |
Merge #1186
1186: Add some docs r=Dirbaio a=Dirbaio
This also does some renames of things to more intuitive/consistent names.
Co-authored-by: Dario Nieuwenhuis <[email protected]>
Diffstat (limited to 'docs')
0 files changed, 0 insertions, 0 deletions