[PATCH] Update --with-gnu-as doc entry

[Eric Botcazou]

> In this particular case, we don't have a cross-reference to another
> option.  What we have is a case where all of the documentation is
> located someplace else.  In this case, a @uref seems clearly better than
> @option, because otherwise it is hard to find the documentation you are
> looking for in the html docs.

Hum... "someplace else" is just above in this case.

> I also suspect that this is a case of incomplete conversion, where
> someone (namely jsm) tried to convert @option to @uref to improve the
> appearance of the documentation, but didn't catch all of the cases that
> mattered.  We shouldn't be going backwards by removing improvements just
> because they are incomplete.

Agreed. May I turn the following --with-ld into an @uref then, as you 
initially suggested?

> Search for --with-gnu-as.  It is 2/3 of the way into the file.

Ah! yes, there are actually two such @uref. But they are not in the options 
section.

-- 
Eric Botcazou