On Fri, Oct 01, 2021 at 01:53:37PM +0200, Richard Biener wrote: > OK. Maybe the change is worth mentioning in changes.html or maybe it's > just a bugfix...
I think it is worth mentioning it there. And so I'd probably wouldn't try to backport it, except perhaps the recover for float-divide-by-zero fix. Jakub