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

I've rebased the branch on the "fixup" commit `v1.11-250-g0c0b402', and
I will merge it to maint (and push) in a couple of days if there is no
objection by then.  The updated patch is attached, for reference.

Regards,
  Stefano