tags 15237 minor
close 15237
stop

Reference:
<http://debbugs.gnu.org/cgi/bugreport.cgi?bug=15237>

Thanks for the report, and sorry for the delay.  This was a
spurious failure, fixed by the attached patch.

Regards,
  Stefano