On Tue, 5 Dec 2023 at 14:44, Jonny Grant <jg@xxxxxxxx> wrote: > > > > On 05/12/2023 04:04, Xi Ruoyao wrote: > > On Mon, 2023-12-04 at 23:22 +0000, Jonny Grant wrote: > > > > /* snip */ > > > >> > >> > >> Thank you and Xi for the link again. > >> > >> > >> I signed up for a wiki account, but I can't see an "edit" button - is > >> there a step I need to follow? Wanted to make a spelling correction on > >> that page "hellgrind". > > > > https://gcc.gnu.org/wiki/EditorGroup > > I see, my username is JonnyGrant, I'm not on the list. > > Could you change "hellgrind" -> "helgrind" ? > https://gcc.gnu.org/wiki/FAQ > > The other change was "feed-back" -> "feedback" > https://gcc.gnu.org/wiki/Community Both fixed, thanks!
