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 Anyway, with git I'd like to say that it is desirable to commit such patches with git commit --author '...' to give due credit. Jakub
