X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Fui%2Fgui%2Fhelp-menu.h;h=4d5e2303e6f4aed03498a38b455d4465111034ff;hb=73a2e47de094934075e66d1e5185fce93d47fe5e;hp=ff3740fba6291c46598272c17fc7211667a82184;hpb=f5ae39af68c25bc004a8a43b288ebc6e00165b03;p=pspp-builds.git

diff --git a/src/ui/gui/help-menu.h b/src/ui/gui/help-menu.h
index ff3740fb..4d5e2303 100644
--- a/src/ui/gui/help-menu.h
+++ b/src/ui/gui/help-menu.h
@@ -22,4 +22,7 @@
 
 void merge_help_menu (GtkUIManager *uim);
 
+void online_help (const char *page);
+
+
 #endif