diff options
| author | Clément Pit-Claudel | 2018-05-16 21:24:47 -0400 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-20 10:12:55 +0200 |
| commit | a63bc54bfd697e76182044a8515818fa8f92e849 (patch) | |
| tree | f1c0b461365586c855e94db7277683dcbe753fea /doc/sphinx/practical-tools | |
| parent | b627c7242d71c834e7a06353ced967c43598e344 (diff) | |
[doc] Fix a few LaTeX mistakes
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/coqide.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index bc6a074a27..e8fc29dece 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -263,7 +263,7 @@ for the ∀ symbol. A list of symbol codes is available at An alternative method which does not require to know the hexadecimal code of the character is to use an Input Method Editor. On POSIX systems (Linux distributions, BSD variants and MacOS X), you can -use `uim` version 1.6 or later which provides a :math:`\LaTeX`-style input +use `uim` version 1.6 or later which provides a LaTeX-style input method. To configure uim, execute uim-pref-gtk as your regular user. In the |