diff options
| author |  gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-15 10:14:10 +0000 |
|---|---|---|
| committer | gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-15 10:14:10 +0000 |
| commit | 0fa64b47f270f9d31d32d499c0f9f8c23f370124 (patch) | |
| tree | 2811edb989a8f0ae102ca52a5bffe3fb7f1bbb53 /doc/refman | |
| parent | 49fc62017f38b242a16e99f9d487c26e58e628d2 (diff) | |
Documentation typo.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14008 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/refman')
| -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 51fe979f5..f061ef18d 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} |