severity 15376 minor
tags 15376 + patch
close 15376
stop

Reference:
http://debbugs.gnu.org/cgi/bugreport.cgi?bug=15376

Hi Tobias, thanks for the report and the patch, and sorry for the
shameful delay.  I've adjusted the problem you reported, plus other
similar issues I noticed along the way, with the attached patch.

Thank you,
  Stefano