10 Jul
2020
10 Jul
'20
12:50 a.m.
When a PR is merged, is it closed automatically or do we need to do something to close it?
-- ~Ethan~