Paolo Bonzini wrote:
I committed this patch as it is pretty obvious.
And I committed a merge in the meanwhile.  Sorry; I'll prepare a patch 
to git to disable merges on branches where you do not want them. :-)
Paolo


Reply via email to