Hi Jonathan, On 11/14/22 16:36, Jonathan Wakely wrote: > 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. It works. I didn't know it existed :) Maybe add a reference to it in the README? Thanks! Alex --