Hey @heusch,
Can you please merge this? Not much to review, just a small bug fix. Thanks!
merged
mentioned in commit d21f4d6c