diff options
Diffstat (limited to 'ide/coqide_ui.ml')
| -rw-r--r-- | ide/coqide_ui.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index 6b464348c..adfd9e668 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -82,7 +82,6 @@ let init () = <menuitem action='Start' /> <menuitem action='End' /> <menuitem action='Interrupt' /> - <menuitem action='Hide' /> <menuitem action='Previous' /> <menuitem action='Next' /> </menu> @@ -145,7 +144,6 @@ let init () = <toolitem action='Start' /> <toolitem action='End' /> <toolitem action='Interrupt' /> - <toolitem action='Hide' /> <toolitem action='Previous' /> <toolitem action='Next' /> <toolitem action='Wizard' /> |