Thanks Toby. I was just logging into my computer to take a look into this, but you beat me to it.
I found and fixed the bug. The according commit just has been pushed
to the git repository - everyone should update.
Thank you very much for reporting this bug!