diff options
Diffstat (limited to 'ide/coqide_ui.ml')
| -rw-r--r-- | ide/coqide_ui.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index c994898a4f..c30d6604d2 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -140,6 +140,8 @@ let init () = \n <menuitem action='Uncomment' />\ \n <separator />\ \n <menuitem action='Coqtop arguments' />\ +\n <separator />\ +\n <menuitem action='Latex-to-unicode' />\ \n </menu>\ \n <menu action='Compile'>\ \n <menuitem action='Compile buffer' />\ |