@folkert does this change fix your compilation errors?
Yes it fixes the compilation errors.
Thanks for confirming this. And sorry about the mistake. We forgot to check that case.
merged
mentioned in commit 7a5efc8c