> Can someone please revert the patch? This is not possible within
> the short time I have now.
Done:
git revert -n HEAD
<edit ChangeLog file>
git add ChangeLog
git commit -a
git push
>> One more reason to move it into a separate branch...
>
> Good, but I cannot do that for some time. Help?
As soon as you find time again, you can move the now reverted commit
to a separate branch. I'm leaving today for a summer course, so I
can't help right now. However, I'm sure you find some guidance in the
net (or other people from the list can assist after they are back from
summer vacation :-).
Werner
