diff options
author | bors[bot] <26634292+bors[bot]@users.noreply.github.com> | 2021-02-07 11:15:26 +0000 |
---|---|---|
committer | GitHub <[email protected]> | 2021-02-07 11:15:26 +0000 |
commit | 336909b63a14b801520c6627d90d750babcfe280 (patch) | |
tree | b5b73fc760b261fafda58a3e20e04b8e74559c60 /.gitignore | |
parent | 75a87ec198b25c5938c651ef087f9ebf923c34f8 (diff) | |
parent | 7022ea52b5f2a0262c2cd96b290ddb8ec0af0df9 (diff) |
Merge #7587
7587: AdtDef -> Adt r=matklad a=matklad
bors r+
🤖
Co-authored-by: Aleksey Kladov <[email protected]>
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions