Hi Nick, > Anyway this is a bug. Please could you open a bugzilla PR for it. I > have a patch to fix the problem, but I would like the problem to be > officially recorded. > Thanks, I have entered it as #9814. Christophe.