<div dir="ltr"><div dir="ltr"><br></div><br><div class="gmail_quote gmail_quote_container"><div dir="ltr" class="gmail_attr">On Fri, 20 Dec 2024 at 09:02, Zoltan Somogyi <<a href="mailto:zoltan.somogyi@runbox.com">zoltan.somogyi@runbox.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><br>
<br>
On Fri, 20 Dec 2024 08:56:29 +1100, Julien Fischer <<a href="mailto:jfischer@opturion.com" target="_blank">jfischer@opturion.com</a>> wrote:<br>
> On Fri, 20 Dec 2024 at 01:41, Zoltan Somogyi <<a href="mailto:zoltan.somogyi@runbox.com" target="_blank">zoltan.somogyi@runbox.com</a>><br>
> wrote:<br>
> > > +@c @cindex Directories<br>
> > > > +@c @cindex Search path<br>
> > > > +@c Append either the named workspace directory,<br>
> > > > +@c or the named library install directory,<br>
> > > > +@c to one of three separate lists of directories to be searched<br>
> > > > +@c for @samp{.int*} and @samp{.module_dep} files.<br>
> > > > +@c Any workspace directory<br>
> > > > +@c named in a @var{--normal-dirs-same} option<br>
> ><br>
> > Should this fully-spelt-out name of the option be followed here by<br>
> > "(synonyms: <list them here>)"?<br>
> ><br>
> <br>
> The synonyms should be listed above anyway, so I don't think you need<br>
> to repeat them inline.<br>
<br>
My reason for proposing that addition was not to introduce the synonyms,<br>
but to clarify that the appearance of those options above *are* synonyms,<br>
as opposed to semantically separate options. I am not sure about whether<br>
just putting a blank line between the groups-of-synonyms would be sufficient<br>
to get that point across. Or I could just add a remark of the form<br>
"(and its abbreviated synonym)" after text that includes the full form<br>
of the option name.</blockquote><div><br></div><div>That last suggestion works.</div><div><br></div><div>Julien.</div></div></div>