Hi Olivier, how do you merge github pull requests into the master branch? In your log statements I only see messages like 'merge branch pr/28', but these are not published branches as I see, I think you create them locally only? How do you create them? And how does github recognize that the pr is merged into the master? The github email says you should add "This closes #30" to the commit message. But I see no such commit messages in your pr merges.
Greetings Martin
