# HG changeset patch
# User Richard M. Stallman <rms@gnu.org>
# Date 1005061609 0
# Node ID a09c65c0b5e2225aaace17372b3b3e86f1ff1994
# Parent  306eea7b9fdccbf866e5658488ed145abab8e5a0
Minor Texinfo usage fix.

diff -r 306eea7b9fdc -r a09c65c0b5e2 man/text.texi
--- a/man/text.texi	Tue Nov 06 15:44:42 2001 +0000
+++ b/man/text.texi	Tue Nov 06 15:46:49 2001 +0000
@@ -1813,10 +1813,10 @@
 
   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 (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.
+menu in the menu bar (use @kbd{@key{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