diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-ide.tex | 16 |
1 files changed, 3 insertions, 13 deletions
diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex index f061ef18d4..e0c6c868f7 100644 --- a/doc/refman/RefMan-ide.tex +++ b/doc/refman/RefMan-ide.tex @@ -209,21 +209,11 @@ Notice that these settings are saved in the file \verb|.coqiderc| of your home directory. A gtk2 accelerator keymap is saved under the name \verb|.coqide.keys|. -This file should not be edited manually: to modify a given menu +It is not recommanded to edit this file manually: to modify a given menu shortcut, go to the corresponding menu item without releasing the mouse button, press the key you want for the new shortcut, and release -the mouse button afterwards. - -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 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. +the mouse button afterwards. If your system does not allow it, you may still +edit this configuration file by hand, but this is more involved. \section{Using unicode symbols} |