What happens if I delete a remote branch that someone else is working on?

I have created a remote branch, that I now want to delete because it is merged back into our integration branch. I do a

git push origin :name_of_branch

to delete the remote branch.

However, unfortunately I was mistaken and one of the other developers actually开发者_开发百科 has local commits originating on that branch. How do I disturb his work, is his changes now in danger when he pulls?

Thanks

---

Pulling never deletes your local branch. If your other developer uses git fetch --prune, his local remote tracking branches (e.g. remote/origin/name_of_branch) would be deleted, but the local version he is working on should stay untouched, and when he pushes them again, the branch would be recreated.

(Though it might be more useful to push the new commits under a new branch name, depending on context.)