On Tue, 8 Sep 2020, Jakub Jelinek wrote:
On Tue, Sep 08, 2020 at 12:16:08PM +0100, Richard Sandiford wrote:Are platform maintainers allowed to push general changes like these? If so I can push soon.Yeah, anyone with commit access can push an approved patch.I've pushed this one yesterday already: https://gcc.gnu.org/g:3fe3efe5c141a88a80c1ecc6aebc7f15d6426f62
Thanks! // Martin
