On Tue, May 19, 2015 at 5:27 AM, Paul Eggert <eggert at cs.ucla.edu> wrote: > Thanks for the bug report. I installed the attached more-elaborate patch > into the experimental version on github. It should fix the problem in a > different way. Thanks for the patch. Works well here. Leonardo