This was fixed initially by commit 0c3dd50eaecbfe2, which is the change suggested in Paolo's comment #6, and then refined by commit a5cb7c5afe717d4.
This was fixed initially by commit 0c3dd50eaecbfe2, which is the change suggested in Paolo's comment #6, and then refined by commit a5cb7c5afe717d4.