user-manual: Replace .menu with .desktop.

diff --git a/doc/user-manual/user.texinfo b/doc/user-manual/user.texinfo
index 307c5ca4ebebe386301f5665a413e75dbdc1f00d..6ef26e691b6ef932b2d85c12b0f4111ea3a0b849 100644 (file)
--- a/doc/user-manual/user.texinfo
+++ b/doc/user-manual/user.texinfo
@@ -3963,10 +3963,10 @@ Users may also want to use the following enhancements in their code.
 
 @itemize @bullet
 @item
-The Debian packaging includes a @file{.menu} file in
+The Debian packaging includes a @file{.desktop} file in
 @url{freedesktop.org} format.  In the right place it makes this Scheme
 available through an icon (a lambda holding a fountain pen) in a
-@file{.menu} aware application launcher.
+@file{.desktop} aware application launcher.
 
 @item
 The installation process includes HTML documentation by default.  In