On 06/10/2012 02:17 PM, Stefano Lattarini wrote: > Reference: <http://debbugs.gnu.org/cgi/bugreport.cgi?bug=10697> > > See the attached patch; I will push it by tomorrow if there is no objection > (and if anyone would like to give it a try on a real project, that would be > much appreciated). > Pushed now (to maint). I'm thus closing this bug report.
Regards, Stefano
