Breaking change for Pull-Requests: Allman style

[d-a-v]

The Allman restyle process had been on the table from a long time before today.
It had been prepared taking into account all ongoing pull-requests.

What was initially planned, which doesn't work, was:

An ongoing PR has to be merged to the commit right before allman commit:
git merge 625c3a62c4991347e8298fb5e4021bc6f6df7099
Then the script tests/restyle-all.sh has to be called.

After that, the diff against master is good, but git merge master conflicts and has to be repaired by hand. And the conflicts are exactly the committed patches (the initial PR before Allman).

Here is a script which will do some git/diff mixture and hopefully be able to update a pull request. Assuming your git remote is called origin, this script can be run from your local directory (linux only) with the pull request number.

We can, on demand, create an updated version of your PR for you.

Check this gist: https://gist.github.com/d-a-v/29b1cf4b54e646df188997c7b3086796