Re: wwwdocs/htdocs/onlinedocs/5.1.0 - New directory

[Gerald Pfeifer]

Hi Jakub,

would this better be gcc.gnu.org/onlinedocs/5.1/ instead of 5.1.0
to be in alignment with the release?

Gerald

PS. I can make this change on gcc.gnu.org (probably using a redirect
for the original link).