aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqide_ui.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coqide_ui.ml')
-rw-r--r--ide/coqide_ui.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index fd5bc6c49..ed8027959 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -141,6 +141,7 @@ let init () =
<menuitem action='Browse Coq Manual' />
<menuitem action='Browse Coq Library' />
<menuitem action='Help for keyword' />
+ <menuitem action='Help for μPG mode' />
<separator />
<menuitem name='Abt' action='About Coq' />
</menu>