tags 8407 + patch
close 8407
thanks

Reference:

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

I've applied the attached patch to maint, and I'm thus closing this bug
report.

Regards, and thanks for the patience,
  Stefano