[jdt-core-dev] once more: egit push accident ... reverted

[Stephan Herrmann <stephan.herrmann@xxxxxxxxx>]

Hi team,

I did it again: click the wrong button in EGit: while working
on a new feature branch sherrmann/ExternalAnnotations I dared
to click on "Commit and Push" believing it would pick up the
remote configuration from the current local branch.
It didn't, it pushed HEAD to origin/master :(

I immediately added a revert commit [1], so I hope no real
damage is done, except for the clutter in our history. Sorry!

best,
Stephan

[1] http://git.eclipse.org/c/jdt/eclipse.jdt.core.git/commit/?id=efd3b1f31e7f6af67fb63e84ece49ae3c1341055