From bbf334b38ae4c57b4d619a8f98acc488077efca4 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Fri, 27 Apr 2012 15:31:30 +0000
Subject: Removed the quasi-useless gtk2rc file and the documentation that went
 with it. Now CoqIDE is not anymore totally irrespectful of the local
 configuration of themes, in particular w.r.t. to menu fonts.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15251 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-ide.tex | 16 +++-------------
 1 file changed, 3 insertions(+), 13 deletions(-)

(limited to 'doc/refman')

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