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.ml4
1 files changed, 4 insertions, 0 deletions
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index 8732cd83b..72bad7926 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -62,6 +62,10 @@ let init () =
<menuitem action='Previous tab' />
<menuitem action='Next tab' />
<separator/>
+ <menuitem action='Zoom in' />
+ <menuitem action='Zoom out' />
+ <menuitem action='Zoom fit' />
+ <separator/>
<menuitem action='Show Toolbar' />
<menuitem action='Show Query Pane' />
<separator/>