
This reverts commit 2226cdb3dacd21dcf7e9836db57ddb9d7936ac43 and d9c93c9f5d71c7e8cecedb2bed39d8d33029baf1. Because Gilles' b17c89c1 committed a few hours ago has the same change, my RP branch had a conflict.
This reverts commit 2226cdb3dacd21dcf7e9836db57ddb9d7936ac43 and d9c93c9f5d71c7e8cecedb2bed39d8d33029baf1. Because Gilles' b17c89c1 committed a few hours ago has the same change, my RP branch had a conflict.