changeset 70195:23205c99093c

[TeX]: Use xresmini.texi instead of xresources.texi.
author Richard M. Stallman <rms@gnu.org>
date Sun, 23 Apr 2006 21:56:28 +0000
parents c26552fcb626
children 874b926e482a
files man/emacs.texi
diffstat 1 files changed, 5 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/man/emacs.texi	Sun Apr 23 21:53:05 2006 +0000
+++ b/man/emacs.texi	Sun Apr 23 21:56:28 2006 +0000
@@ -1544,7 +1544,12 @@
 
 @include doclicense.texi
 @include cmdargs.texi
+@iftex
+@include xresmini.texi
+@end iftex
+@ifnottex
 @include xresources.texi
+@end ifnottex
 
 @include anti.texi
 @include macos.texi