X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Fui%2Fgui%2Fhelp-menu.c;h=33a9407f71fc8532930b91c9db2fd1f3f407a531;hb=3c5630105991133a09971a4c107141767a2c7d0c;hp=e670c0b555b5b80f0ab5110dff05474d950408fb;hpb=ad9374fb26300c7d6c72b358b6ee9f0b6e5b5c87;p=pspp

diff --git a/src/ui/gui/help-menu.c b/src/ui/gui/help-menu.c
index e670c0b555..33a9407f71 100644
--- a/src/ui/gui/help-menu.c
+++ b/src/ui/gui/help-menu.c
@@ -132,7 +132,7 @@ merge_help_menu (GtkUIManager *uim)
     
       {
 	"help_reference", "help-reference-manual",            /* name, stock id */
-	N_("_Reference Manual"), NULL,               /* label, accelerator */
+	N_("_Reference Manual"), "F1",               /* label, accelerator */
 	NULL,                                        /* tooltip */
 	G_CALLBACK (reference_manual)
       },