On 17.08.2021 6:45, Daniel Shahaf wrote:
Could you file an issue?
I decided to study it a bit more and found more problems, see the newer mail I sent today. For the reasons described there, I decided to abandon the patch: it only fixes half of the problem. While it's already something, I'm out of steam to solve both halves.