Relying on git doesn't work in awful lot of cases, e.g. when there's a
shallow `git clone`.
Instead have "hardcoded" version in files, and update it before release.
Closes#4165.
Add missing copyright stuff to `merge-pr.sh`.
Refactored & split `merge-pr.sh` script, since most of required
code for `test-pr.sh` already existed there.
Differences from `merge-pr.sh`:
* if there's no `upstream` remote, https version is used instead of
git
* merge commit *is not* GPG-signed (less hassle)
* merge branch is named e.g. `test1234` instead of `merge1234`
* instructions for pushing test branch onto upstream master are not
printed