diff options
| author | herbelin | 2007-05-17 14:55:44 +0000 |
|---|---|---|
| committer | herbelin | 2007-05-17 14:55:44 +0000 |
| commit | c77c470dbecd9c5a8435995515ebac8336a6591a (patch) | |
| tree | 50c1d869f38c4cb85503f9a021ff68d644542d00 | |
| parent | 01eb823bc346f06e0a075a9dc2bbf6aa9e70b2d1 (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.tex | 9 |
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 |
