diff options
author | bors[bot] <26634292+bors[bot]@users.noreply.github.com> | 2020-12-29 13:15:07 +0000 |
---|---|---|
committer | GitHub <[email protected]> | 2020-12-29 13:15:07 +0000 |
commit | 343029fa9e52cf4aae7f17ed6e0e6b5b0175a172 (patch) | |
tree | 004195234e0409ddc54514a2e8b737ed8e16b74e /.github/workflows/metrics.yaml | |
parent | ef1177c5b5a7ced9866025a51c10e4375e2a37fd (diff) | |
parent | 42c24ff25f391a1e3662ce226d510aedc9d1f0e4 (diff) |
Merge #7077
7077: Avoid a couple of allocations r=Veykril a=lnicola
r? @Veykril
TBH I'm not sure this is worth it, but the other `Query` was already taking a `String`.
Co-authored-by: Laurențiu Nicola <[email protected]>
Diffstat (limited to '.github/workflows/metrics.yaml')
0 files changed, 0 insertions, 0 deletions