When 546ec1a5 was merged into develop, I accidentally overwrote the change
introduced in debbea5b (pr #1657). Reintroduce it.