gitでローカルブランチと名前の異なるリモートブランチにpushする

試した環境

本題

例えばローカルのdevという名前のブランチの内容をリモートのdevelopという名前のブランチにpushする場合、以下のコマンドで実行します。

git push origin dev:develop

-uオプションを使ってgit push -u origin dev:developのようにしても、次にgit pushコマンドを実行しても失敗します。

$ git push
fatal: The upstream branch of your current branch does not match
the name of your current branch.  To push to the upstream branch
on the remote, use

    git push origin HEAD:develop

To push to the branch of the same name on the remote, use

    git push origin HEAD

To choose either option permanently, see push.default in 'git help config'.

To avoid automatically configuring an upstream branch when its name
won't match the local branch, see option 'simple' of branch.autoSetupMerge
in 'git help config'.

参考

https://git-scm.com/docs/git-push#Documentation/git-push.txt-codegitpushoriginHEADmastercode