No commit on PR merge

[aremazeilles]

Ping @alfonsotecnalia

I guess I updated this fork through the Github interface, but when bringing here the latest updates from the main repo, a commit got created. I think this should be avoided as it is then difficult to make sure the two branches (base fork) are synch.

Th way I solved it in beat was to undo the last commit, and force this update the remote.
I can do it again.
But it would be good to have the procedure for doing it directly and correctly from the github interface.
There are several merging options in the github interface, we should check if one is better than the other.