This is an old revision of the document!
GIT Tips & Tricks
Different local username
If your SSH username is not the same as your local username, you can make an entry in $HOME/.ssh/config
(create it if it doesn't exist) so you don't have to type it each time:
Host git.xfce.org User $USERNAME
Pull over git:// push with ssh://
You can switch to a different protocol or location for the push command. Advantage is that you can clone a repository using git://git.xfce.org/... which is faster than a ssh connection (no login, permission check and encryption), but push to ssh.
- .gitconfig
[url "ssh://git@git.xfce.org"] pushInsteadOf = "git://git.xfce.org"