This commit amends 9897afa5.

Changes were pushed to the wrong branch, so the MR got merged not in its
final state.

(cherry picked from commit 3af565b6)