Huh, I guess Github isn't smart enough to figure out that that commit was a manual merge of the PR, so it shows up as "closed" instead of "merged". But don't worry, the actual changes are merged :)

Also, I fixed up the author name on your commit to use your full name; that is good practice, so you may want to update your git config to do this by default. See https://help.github.com/en/github/using-git/setting-your-username-in-git

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub, or unsubscribe.