Revert "Make nicer pull request merge messages"
This reverts commit 1078fb08851442bcd7750c3d5015dc1fe7e4d927 (and thus
pull #5623). It has various issues:
- Pull request names get cut off at ", see e.g. a026a56
- Merge script no longer copes with pulls that have a milestone attached, due to a duplicate 'title' in JSON that is not handled by the ad-hoc parsing.