Correct error introduced in previous commit: Forgot to commit modification which goes together with the change in [8587]