# HG changeset patch
# User Richard M. Stallman <rms@gnu.org>
# Date 1005022396 0
# Node ID d2264ed210a7179342b230dfc98aba36bb9f43a0
# Parent  f336a6703f790e7860fbc074c015251ec7afc4d1
Along with Text Properties menu, mention keyboard commands
in following section.

diff -r f336a6703f79 -r d2264ed210a7 man/text.texi
--- a/man/text.texi	Tue Nov 06 04:51:53 2001 +0000
+++ b/man/text.texi	Tue Nov 06 04:53:16 2001 +0000
@@ -1811,10 +1811,12 @@
   There are two ways to alter the formatting information for a formatted
 text file: with keyboard commands, and with the mouse.
 
-  The easiest way to add properties to your document is by using the Text
+  The easiest way to add properties to your document is with the Text
 Properties menu.  You can get to this menu in two ways: from the Edit
-menu in the menu bar, or with @kbd{C-Mouse-2} (hold the @key{CTRL} key
-and press the middle mouse button).
+menu in the menu bar (use @kbd{F10 e t} if you have no mouse), or with
+@kbd{C-Mouse-2} (hold the @key{CTRL} key and press the middle mouse
+button).  There are also keyboard commands described in the following
+section.
 
   Most of the items in the Text Properties menu lead to other submenus.
 These are described in the sections that follow.  Some items run