X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Fui%2Fgui%2Fhelp-menu.c;h=33a9407f71fc8532930b91c9db2fd1f3f407a531;hb=d6fb2728eb8a99e89165c45d8e5d4a482114d3a0;hp=e670c0b555b5b80f0ab5110dff05474d950408fb;hpb=56231bc7e8c2cda46a69d10362193556dd8cad41;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)
       },