Again, the problem is making the changelog update optional! No pull request should be merged if it doesn't include a proper changelog entry,that's how it's done.
We tried that in the past, and it lead to tons of merging errors. They are easy to resolve manually, of course, but still very annoying because this breaks the GitHub "Merge" button.
David
