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

So here is a proposed patch (for maint).  I will push in 72 hours if there is no
objection.

Regards,
  Stefano