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

2 files changed, 9 insertions, 0 deletions

diff --git a/man/ChangeLog b/man/ChangeLog
index 4874557a692..6d5aeb9ede8 100644
--- 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 c926961891f..4e01af2a27a 100644
--- 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