diff options
| author | bors[bot] <26634292+bors[bot]@users.noreply.github.com> | 2021-03-16 16:58:48 +0000 |
|---|---|---|
| committer | GitHub <[email protected]> | 2021-03-16 16:58:48 +0000 |
| commit | 4771a5f1ca810a3f3697aea8da5af6dc8c03bbd1 (patch) | |
| tree | dc4ed41e25efae7b6f76fcf18b6b6eb68170e7a9 /bench_data | |
| parent | 00c80b208bcbe52b13bbd03cb62e24b2d2075edf (diff) | |
| parent | ce2cae45b5242d59b744018dd79bc2ab74670edc (diff) | |
Merge #8041
8041: Rename Substs -> Substitution r=flodiebold a=flodiebold
Co-authored-by: Florian Diebold <[email protected]>
Diffstat (limited to 'bench_data')
0 files changed, 0 insertions, 0 deletions