Hi @Michael,
yes, it would be great if the bug could be fixed once and for all. However, I just passed on the solution @jon once posted here and don’t know its implications. Since @jon didn’t make a pull request then, I assumed that there was a reason for that line and always warned people that changing it might have unexpected consequences.