Failed to make v10 branch: gitmaster push hook needs adjustment

So I just tried to make the v10 branch, and was given the raspberry:

$ git push origin master:refs/heads/REL_10_STABLE
Total 0 (delta 0), reused 0 (delta 0)
remote: Branch refs/heads/REL_10_STABLE violates the policy: Branch name does not match allowed regexp
remote: error: hook declined to update refs/heads/REL_10_STABLE
To ssh://git(at)gitmaster(dot)postgresql(dot)org/postgresql.git
! [remote rejected] master -> REL_10_STABLE (hook declined)
error: failed to push some refs to 'ssh://git(at)gitmaster(dot)postgresql(dot)org/postgresql.git'

Presumably, there's some bit of logic there that's expecting two numeric
portions and no underscore just after REL. Somebody please update it to
expect the format REL_\d+_STABLE for future branch names.

regards, tom lane