aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorherbelin2007-05-17 14:55:44 +0000
committerherbelin2007-05-17 14:55:44 +0000
commitc77c470dbecd9c5a8435995515ebac8336a6591a (patch)
tree50c1d869f38c4cb85503f9a021ff68d644542d00
parent01eb823bc346f06e0a075a9dc2bbf6aa9e70b2d1 (diff)
Fixed bug #1540 (typo on name .coqide-gtk2rc)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9828 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--doc/refman/RefMan-ide.tex9
1 files changed, 6 insertions, 3 deletions
diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex
index f24d79e28c..fa66d8336d 100644
--- a/doc/refman/RefMan-ide.tex
+++ b/doc/refman/RefMan-ide.tex
@@ -207,7 +207,10 @@ For experts: it is also possible to set up a specific gtk resource
file, under the name \verb|.coqide-gtk2rc|, following the gtk2
resources syntax
\url{http://developer.gnome.org/doc/API/2.0/gtk/gtk-Resource-Files.html}.
-Such a default resource file exists in the \Coq{} library, you may
+Such a default resource file can be found in the subdirectory
+\verb=lib/coq/ide= of the root installation directory of \Coq{}
+(alternatively, it can be found in the subdirectory \verb=ide= of the
+source archive of \Coq{}). You may
copy this file into your home directory, and edit it using any text
editor, \CoqIDE{} itself for example.
@@ -256,7 +259,7 @@ $\forall$ and $\exists$ respectively, you may add
bind "F11" {"insert-at-cursor" ("$\forall$")}\\
bind "F12" {"insert-at-cursor" ("$\exists$")}
\end{quote}
-to your \verb|binding "text"| section in \verb|.coqiderc-gtk2rc|.
+to your \verb|binding "text"| section in \verb|.coqide-gtk2rc|.
% such a binding is system-dependent. We
@@ -275,7 +278,7 @@ to your \verb|binding "text"| section in \verb|.coqiderc-gtk2rc|.
% bind "F13" {"insert-at-cursor" ("$\forall$")}\\
% bind "F14" {"insert-at-cursor" ("$\exists$")}
% \end{quote}
-% to your \verb|binding "text"| section in \verb|.coqiderc-gtk2rc|.
+% to your \verb|binding "text"| section in \verb|.coqide-gtk2rc|.
% The strange \verb|∀| argument is the UTF-8 encoding for
% 0x2200, that is the symbol $\forall$. Computing UTF-8 encoding
% for a unicode can be done in various ways, including