message no. 177674
Posted by dmlloyd in #github at 2020-03-12T18:12:32Z
if you manually merge it, and push that up, github should automatically close the PR as "merged"
Posted by dmlloyd in #github at 2020-03-12T18:12:32Z