diff options
| author | charguer | 2018-11-13 11:12:51 +0100 |
|---|---|---|
| committer | Vincent Laporte | 2019-03-18 10:29:51 +0000 |
| commit | 5ad4ed36e09416e8e4aa16f67b517eec78591532 (patch) | |
| tree | 937c7e2d51c5d39e4ce9ebe3c12afc5b77c1aeec | |
| parent | ea789fb00cecbb720702940d4752e991bbcc2054 (diff) | |
Latex to LaTex
| -rw-r--r-- | ide/coqide.ml | 2 | ||||
| -rw-r--r-- | ide/coqide_ui.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index e79e11540e..8e62ac9193 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1165,7 +1165,7 @@ let build_ui () = ~callback:MiscMenu.uncomment; item "Coqtop arguments" ~label:"Coqtop _arguments" ~callback:MiscMenu.coqtop_arguments; - item "Latex-to-unicode" ~label:"_Latex-to-unicode" ~accel:"<Shift>space" + item "LaTeX-to-unicode" ~label:"_LaTeX-to-unicode" ~accel:"<Shift>space" ~callback:MiscMenu.apply_unicode_binding; ]; 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' />\ |