This is difficult to fix and perhaps not worth fixing.

We will leave the ticket open for the time being as a record of the problem,
but we do not anticipate fixing it right away.