When are pull requests closed on Github?

[Xiao Jia]

I noticed that after Barret merged our changes, the corresponding pull
requests are still open. Are we supposed to close them on the Github
website?

Also Barret's replies were showed up as Github user akaros-notifier.
Is this the intended behavior?

[Kevin Klues]

In general, github is pretty good about recognizing when to close a
pull-request even if it is rebased (so its sha1 changes) instead of
merged. Unfortunately, to do this they match the text of the final
commit message. Since our commit messages change with Barret's final
sign-off, there is no way for github to recognize the merge
automatically. In the past I've added a final comment saying "merged
as a2bc3df" and then closed it manually.

The replies as "akaros-notifier" are not intended. I'll look into it.

> --
> You received this message because you are subscribed to the Google Groups "Akaros" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to akaros+un...@googlegroups.com.
> To post to this group, send email to aka...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.



--
~Kevin