On Wed, 6 Dec 2023, 21:49 Jonny Grant, <jg@xxxxxxxx> wrote: > > > 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. It doesn't actually need to be outside the source directory. It can't be a parent of the source directory though. 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 I don't think the official/formal manual links to the informal wiki. >
