diff options
| -rw-r--r-- | doc/refman/RefMan-ide.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex index 51fe979f56..f061ef18d4 100644 --- a/doc/refman/RefMan-ide.tex +++ b/doc/refman/RefMan-ide.tex @@ -270,7 +270,7 @@ To configure \texttt{uim}, execute \texttt{uim-pref-gtk} as your regular user. In the "Global Settings" group set the default Input Method to "ELatin" (don't forget to tick the checkbox "Specify default IM"). In the "ELatin" group set the layout to "TeX", and remember the content of the "[ELatin] on" field (by default -"<Control>\"). You can now execute CoqIDE with the following commands (assuming +"<Control>\textbackslash"). You can now execute CoqIDE with the following commands (assuming you use a Bourne-style shell): \begin{verbatim} |