aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorgmelquio2011-04-15 10:14:10 +0000
committergmelquio2011-04-15 10:14:10 +0000
commit0fa64b47f270f9d31d32d499c0f9f8c23f370124 (patch)
tree2811edb989a8f0ae102ca52a5bffe3fb7f1bbb53
parent49fc62017f38b242a16e99f9d487c26e58e628d2 (diff)
Documentation typo.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14008 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--doc/refman/RefMan-ide.tex2
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}