diff options
author | bors[bot] <26634292+bors[bot]@users.noreply.github.com> | 2021-03-08 21:19:31 +0000 |
---|---|---|
committer | GitHub <[email protected]> | 2021-03-08 21:19:31 +0000 |
commit | c48478621fe9b50cb19bfd0ea4a5c2ff0de5d6ac (patch) | |
tree | 3905029a42c8bb6c5d363753b34cd6b5dd43f4d5 /docs/user | |
parent | c5189a22ccf4c28e309e4189defbb88b83bb2aea (diff) | |
parent | fc9eed4836dfc88fe2893c81b015ab440cea2ba6 (diff) |
Merge #7924
7924: Use upstream cov-mark r=matklad a=lnicola
Closes #7922
But doesn't remove any dependency, unfortunately.
Co-authored-by: Laurențiu Nicola <[email protected]>
Diffstat (limited to 'docs/user')
0 files changed, 0 insertions, 0 deletions