From c77c470dbecd9c5a8435995515ebac8336a6591a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 17 May 2007 14:55:44 +0000
Subject: 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
---
 doc/refman/RefMan-ide.tex | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'doc')

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
-- 
cgit v1.2.3