This should have been removed in 06440ef57b3a7d868de93dae694ec542218db092, but was probably forgotten. Solves #6718.