git push origin BRANCHNAME question

I think I understand this from the git-push man page, but I want to make 
sure:

I have two branches, master and develop.

If I am (accidentally) sitting on master, and issue 'git push origin 
develop', does this properly push develop to remote develop, or does it 
push master to remote develop (which seems to be bad, in the most common 
use case.)  ?

Thanks,

Ed


-- 
Ed Greenberg
Glens Falls, NY USA