Reference: <http://debbugs.gnu.org/11791>
On 06/27/2012 03:08 PM, Stefano Lattarini wrote: > > I agree. The attached patch should solve the issue. It's more ugly > than I'd like, but this bug is annoying enough to make such ugliness > acceptable. I will push (to maint) in a couple of days if there are > no objections. > Pushed now. I'm thus closing this bug report. Regards, Stefano
