On Mon, 14 Nov 2022 at 15:03, Alejandro Colomar wrote: > BTW, it might be interesting to provide that manual > in a package, so that I could install it as something like: > > apt-get install gcc-doc-internal
"info gccint" already works fine on my distro. If it's not packaged for yours, that's a distro issue.
