diff options
| author | Sandra Loosemore <sandra@codesourcery.com> | 2023-03-11 00:40:42 +0000 |
|---|---|---|
| committer | Sandra Loosemore <sandra@codesourcery.com> | 2023-03-11 01:13:34 +0000 |
| commit | c62df15d283f035d5b1644f74493db2933f2a8cb (patch) | |
| tree | b105a299f00635bb8cbd326713a43b78488e98f6 /gcc/doc/install.texi2html | |
| parent | c80654412b57b35620478cb139debe615ddbf8de (diff) | |
| download | gcc-c62df15d283f035d5b1644f74493db2933f2a8cb.zip gcc-c62df15d283f035d5b1644f74493db2933f2a8cb.tar.gz gcc-c62df15d283f035d5b1644f74493db2933f2a8cb.tar.bz2 | |
Docs: Update documentation of Texinfo versions for building manuals.
There has been recent discussion on updating the minimum required
version of Texinfo from the current version 4.7. This patch does not
do that, but it suggests that people use a more recent version to get
better output. It also removes some other references to Texinfo 4.7
and fixes some related bit-rot in the installation manual. (Nobody
really wants to print the GCC manual any more, and the GCC web site
is a better place to get prebuilt manuals than the FSF store.)
gcc/ChangeLog:
* doc/install.texi (Prerequisites): Suggest using newer versions
of Texinfo.
(Final install): Clean up and modernize discussion of how to
build or obtain the GCC manuals.
* doc/install.texi2html: Update comment to point to the PR instead
of "makeinfo 4.7 brokenness" (it's not specific to that version).
Diffstat (limited to 'gcc/doc/install.texi2html')
| -rwxr-xr-x | gcc/doc/install.texi2html | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/gcc/doc/install.texi2html b/gcc/doc/install.texi2html index f3878aa..54e27fe 100755 --- a/gcc/doc/install.texi2html +++ b/gcc/doc/install.texi2html @@ -53,7 +53,7 @@ do define=`echo $x | sed -e 's/\.//g'` echo "define = $define" $MAKEINFO --no-number-sections -I $SOURCEDIR -I $SOURCEDIR/include -I $DESTDIR $SOURCEDIR/install.texi --html --no-split -D$define -o$DESTDIR/temp.html - # Use sed to work around makeinfo 4.7 brokenness. + # Use sed to work around PR web/88578. sed -e 's/_002d/-/g' -e 's/_002a/*/g' $DESTDIR/temp.html > $DESTDIR/$x rm $DESTDIR/temp.html done |