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