Peter and Martijn propose this change (see the commit message for more information).
ping @p.e.m.taschner @j.f.j.laros