[TeX]: Use xresmini.texi instead of xresources.texi.

diff --git a/man/ChangeLog b/man/ChangeLog
index 4874557a69201b7e1fdc5f30a7a05a24770e7cf3..6d5aeb9ede8033205b2993b847e8a0bb2cb345ef 100644 (file)
--- a/man/ChangeLog
+++ b/man/ChangeLog
@@ -1,5 +1,9 @@
 2006-04-23  Richard Stallman  <rms@gnu.org>
 
+       * emacs.texi [TeX]: Use xresmini.texi instead of xresources.texi.
+
+       * xresmini.texi: New file.
+
        * xresources.texi (Face Resources): Split table into font resources
        and the rest.  Combine similar attributes for brevity.
 

diff --git a/man/emacs.texi b/man/emacs.texi
index c926961891f55309b722bd32f0bd0aef2be8de3d..4e01af2a27ac849edbb77024913a6bbda85ab1b3 100644 (file)
--- a/man/emacs.texi
+++ b/man/emacs.texi
@@ -1544,7 +1544,12 @@ Public License instead of this License.
 
 @include doclicense.texi
 @include cmdargs.texi
+@iftex
+@include xresmini.texi
+@end iftex
+@ifnottex
 @include xresources.texi
+@end ifnottex
 
 @include anti.texi
 @include macos.texi