tags 8461 patch
close 8461
thanks

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

I've decided to go with the third option listed there; attached is the
patch I've pushed to maint.

Regards,
  Stefano