I didn't actually see Lennart's comment 20 two years ago, sorry. Downgrading priority as the actual bug has been fixed two years ago. What's left is some robustification which I outlined in the last paragraph of comment 19.
I didn't actually see Lennart's comment 20 two years ago, sorry. Downgrading priority as the actual bug has been fixed two years ago. What's left is some robustification which I outlined in the last paragraph of comment 19.