Sorry for deleting a file by mistake during the last merge, which would cause errors.
Ok, sounds good.
merged
mentioned in commit 6d0bf33f