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