On 05/12/2023 14:49, Jonathan Wakely wrote: > 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! Great! https://gcc.gnu.org/wiki/FAQ#configure Current: "Then make a peer gcc-build directory next to the GCC source code directory. This should be an empty directory before you start." I suggest changing "peer" -> "separate" and "next to" -> "outside" ie: "Then make a separate gcc-build directory outside to the GCC source code directory. This should be an empty directory before you start." I was thinking of submitting a patch to add a link to https://gcc.gnu.org/wiki/FAQ to https://gcc.gnu.org/install/configure.html Cheers, Jonny
