(code changes have already been merged separately).

Use this occasion to fix the branch name in the configuration file.