aboutsummaryrefslogtreecommitdiffhomepage
path: root/INSTALL.ide
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-01-07 17:01:29 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-01-07 17:01:29 +0000
commit591e7ae9f979190a1ccaf9df523f6b73b1e6536a (patch)
tree470435cd740b9c46c681741777aa781deac656b6 /INSTALL.ide
parentf017a050a405334578a24569fba1b3010b6f191b (diff)
Ajout d'une explication dans la FAQ pour le bug avec MOD4 sous Coqide
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10431 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'INSTALL.ide')
-rw-r--r--INSTALL.ide14
1 files changed, 14 insertions, 0 deletions
diff --git a/INSTALL.ide b/INSTALL.ide
index 029ec03ce..5a4a62238 100644
--- a/INSTALL.ide
+++ b/INSTALL.ide
@@ -115,3 +115,17 @@ There are three configuration files located in your $(HOME) dir.
to change the default shortcuts for the menus.
Read ide/FAQ for more informations.
+
+
+TROUBLESHOOTING
+
+ - Problem with automatic templates
+
+ Some users may experiment problems with unwanted automatic
+ templates while using Coqide. This is due to a change in the
+ modifiers keys available through GTK. The straightest way to get
+ rid of the problem is to edit by hand your .coqiderc (either
+ /home/<user>/.coqiderc under Linux, or
+ C:\Documents and Settings\<user>\.coqiderc under Windows)
+ and replace any occurence of MOD4 by MOD1.
+