Miklos,<div><br></div><div>&gt; <span style="background-color:rgb(255,255,255);white-space:pre-wrap">Except this: is this really needed? As far as I see, it&#39;s not used.</span></div><div><span style="white-space:pre-wrap">You are correct, of course. I had added those lines before I fully understood how the code worked, and forgotten to remove them. I have updated my patch and formatted it correctly.</span></div>