All the credit goes to Paulo Matos who carefully worked out and tested this fix, and updated the patch several times over more than a year while I very slowly got around to reviewing it and checking it in.