Gerald Pfeifer <ger...@pfeifer.com> writes: > If it's not used any more, yes, please go ahead an remove it.
Done as this, tested with make info. Andreas. * doc/include/gpl.texi: Remove. * doc/sourcebuild.texi (Texinfo Manuals): Don't mention gpl.texi. diff --git a/gcc/doc/include/gpl.texi b/gcc/doc/include/gpl.texi deleted file mode 100644 index bcb5535..0000000 [omitted] diff --git a/gcc/doc/sourcebuild.texi b/gcc/doc/sourcebuild.texi index 3d834ee..dc5cc47 100644 --- a/gcc/doc/sourcebuild.texi +++ b/gcc/doc/sourcebuild.texi @@ -1,4 +1,4 @@ -@c Copyright (C) 2002, 2003, 2004, 2005, 2007, 2008, 2009, 2010, 2011 +@c Copyright (C) 2002, 2003, 2004, 2005, 2007, 2008, 2009, 2010, 2011, 2012 @c Free Software Foundation, Inc. @c This is part of the GCC manual. @c For copying conditions, see the file gcc.texi. @@ -368,8 +368,7 @@ The GNU Free Documentation License. The section ``Funding Free Software''. @item gcc-common.texi Common definitions for manuals. -@item gpl.texi -@itemx gpl_v3.texi +@item gpl_v3.texi The GNU General Public License. @item texinfo.tex A copy of @file{texinfo.tex} known to work with the GCC manuals. -- 1.7.11.1 -- Andreas Schwab, sch...@linux-m68k.org GPG Key fingerprint = 58CA 54C7 6D53 942B 1756 01D3 44D5 214B 8276 4ED5 "And now for something completely different."