branch master updated: * doc/texinfo.texi (small): Mention "@set dispenvsize small" and possibility of CSS for HTML output.

[Gavin D. Smith]

This is an automated email from the git hooks/post-receive script.

gavin pushed a commit to branch master
in repository texinfo.

The following commit(s) were added to refs/heads/master by this push:
     new 725b3fe783 * doc/texinfo.texi (small): Mention "@set dispenvsize 
small" and possibility of CSS for HTML output.
725b3fe783 is described below

commit 725b3fe783082519ebd8516cc2343f64327030bf
Author: Gavin Smith <gavinsmith0123@gmail.com>
AuthorDate: Sun Nov 10 12:59:17 2024 +0000

    * doc/texinfo.texi (small): Mention "@set dispenvsize small" and
    possibility of CSS for HTML output.
---
 ChangeLog        | 5 +++++
 doc/texinfo.texi | 7 ++++++-
 2 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/ChangeLog b/ChangeLog
index 2d56f5c06d..98ac29f78e 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,8 @@
+2024-11-10  Gavin Smith <gavinsmith0123@gmail.com>
+
+       * doc/texinfo.texi (small): Mention "@set dispenvsize small" and
+       possibility of CSS for HTML output.
+
 2024-11-09  Gavin Smith <gavinsmith0123@gmail.com>
 
        * doc/texinfo.texi (HTML Output Structure Customization): Clarify
diff --git a/doc/texinfo.texi b/doc/texinfo.texi
index 136935d630..2f76585624 100644
--- a/doc/texinfo.texi
+++ b/doc/texinfo.texi
@@ -6638,9 +6638,14 @@ a fixed-width font, and everything else uses the regular 
font.
 They also have the same behavior in other respects---whether filling
 is done and whether margins are narrowed.
 
+@vindex dispenvsize
 As a general rule, it's better to just use the regular
 commands (such as @code{@@example} instead of @code{@@smallexample}),
-unless you have a good reason for it.
+unless you have a good reason for it.  When processing with
+@file{texinfo.tex} only, you can obtain a similar effect with
+@samp{@@set dispenvsize small}, which uses a smaller font for
+@code{@@example} and other environments.  In HTML output, you can
+use CSS to change the font size of enviroments if needed; @pxref{HTML CSS}.
 
 
 @node Lists and Tables