Hi Gerald.
I noticed that https://gcc.gnu.org does not have a news item related
to this contribution. Would you mind adding one? (Our web pages are
now in GIT, cf. https://gcc.gnu.org/about.html - let me know if you need
help.)
Done! :)
