In this way, we also gain an explicit place for the default setting (still not filled in). No functional changes. This is in preparation of a future commit by Paul Tiedke.